jcommelin

This document is kept around for historical purposes. Instead, please look at

• https://lean-lang.org/lean4/doc/quickstart.html, and/or
• https://leanprover-community.github.io/get_started.html#regular-install

---

---

---

---

---

jcommelin

import tactic
import tactic.find
import init.function
import algebra.group
import group_theory.subgroup

open function

section five_lemma

jcommelin

import tactic
import tactic.find
import init.function
import algebra.group
import group_theory.subgroup

open function

section five_lemma

jcommelin

import data.nat.prime
import algebra.group_power
import tactic.ring

universes u v

namespace nat

class Prime :=
(p : ℕ) (pp : nat.prime p)

jcommelin

import data.nat.prime
import algebra.group_power
import tactic.ring
import linear_algebra.multivariate_polynomial
import ring_theory.localization

universes u v w u₁

-- ### FOR_MATHLIB
-- everything in this section should move to other files

jcommelin

-- Written by Johan Commelin; golfed by Kenny Lau

import tactic.interactive

universe u

namespace eckmann_hilton
variables (X : Type u)

local notation a `<`m`>` b := @has_mul.mul X m a b

jcommelin

#!/bin/python3

### Read a replacement script from stdin
### Read a filename from commandline args
### Output to stdout

### Replacement script has the following form

# ----eofmarker
# line:col:line:col

jcommelin

import category_theory.examples.topological_spaces
import order.lattice order.galois_connection
import category_theory.tactics.obviously

universes u v

open category_theory
open category_theory.examples

namespace open_set

jcommelin

-- Big thanks to Simon Hudon for dictating this file to me
-- and explaining what's going on!

import category_theory.concrete_category

namespace string

def camel_case (s : string) : string :=
(join $ split (λ c, c = '_') s) ++ "'"
  -- TODO make first char uppercase of each elem in list

jcommelin

import data.real.basic

structure complex :=
(re : ℝ)
(im : ℝ)

-- type ℝ as \R
-- type ℂ as \com or \Com

notation `ℂ` := complex