Theorem {u}
Modification history
2023-05-30 23:18
counterexamples/girard.lean
chore(archive + counterexamples): namespaces imo, theorems_100, counterexample, plus three more (#19129) …
Deleted {u}View on Github →2023-03-14 18:20
src/order/initial_seg.lean
feat(order/initial_seg): add lemmas about `acc` and `well_founded` (#18527)
Added {u}View on Github →2023-02-02 14:06
counterexamples/quadratic_form.lean
feat(counterexamples/quadratic_form): symmetric bilinear forms in char 2 do not always inject into quadratic forms (#18146)
Added {u}View on Github →2021-04-06 05:50
src/logic/girard.lean
feat(logic/girard): Girard's paradox (#7026) …
Added {u}View on Github →2021-03-25 10:59
src/logic/basic.lean
feat(logic/basic, logic/function/basic): make `cast` the simp-normal form of `eq.mp` and `eq.mpr`, add lemmas (#6834) …
Deleted {u}View on Github →2019-03-05 14:15
src/logic/basic.lean
feat(topology): split uniform_space and topological_structure
Modified {u}View on Github →2018-10-15 13:39
analysis/topology/quotient_topological_structures.lean
refactor(analysis/topology): move separation ring to quotient_topological_structures
Added {u}View on Github →2017-09-03 20:55
logic/basic.lean
refactor(logic/basic): refactor logic theorems
Deleted {u}View on Github →2017-08-02 16:24
tactic/finish.lean
refactor(*): move theorems and do minor polishing
Deleted {u}View on Github →