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

#!/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

-- 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

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

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 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

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

---

---

---

---

---