Commit 2019-11-12 18:51 1749a8dd
View on Github →feat(group_theory/submonoid): add bundled submonoids and various lemmas (#1623)
- WIP -- removing and everything is broken
- test
- test
- tidy
- fixed localization
- starting on coset
- WIP
- submonoid.lean now compiles but no to_additive stuff
- submonoid.lean compiles
- putting is_submonoid back
- docstrings
- terrible docstrings up to line 370
- finished docstrings
- more to_additive stuff
- WIP -- removing and everything is broken
- test
- test
- tidy
- fixed localization
- starting on coset
- WIP
- submonoid.lean now compiles but no to_additive stuff
- submonoid.lean compiles
- putting is_submonoid back
- docstrings
- terrible docstrings up to line 370
- finished docstrings
- more to_additive stuff
- WIP quotient monoids
- quotient monoids WIP
- quotient_monoid w/o ideals.lean all compiles
- removing lemma
- adjunction
- some tidying
- remove pointless equiv
- completion compiles (very slowly)
- add lemma
- tidying
- more tidying
- mul -> smul oops
- might now compile
- tidied! I think
- fix
- breaking/adding stuff & switching branch
- add Inf relation
- removing sorrys
- nearly updated quotient_monoid
- updated quotient_monoid
- resurrecting computability
- tidied congruence.lean, added some docstrings
- extending setoids instead, WIP
- starting Galois insertion
- a few more bits of to_additive and docs
- no battery
- up to line 800
- congruence'll compile when data.setoid exists now
- more updates modulo existence of data.setoid
- rearranging stuff
- docstrings
- starting additive docstrings
- using newer additive docstring format in submonoid
- docstrings, tidying
- fixes and to_additive stuff, all WIP
- temporary congruence fixes
- slightly better approach to kernels, general chaos
- aahh
- more mess
- deleting doomed inductive congruence closure
- many fixes and better char pred isoms
- docstrings for group_theory.submonoid
- removing everything but bundled submonoids/lemmas
- removing things etc
- removing random empty folder
- tidy
- adding lemma back
- tidying
- responding to PR comments
- change 2 defs to lemmas
- @[simp] group_power.lean lemmas
- responding to commute.lean comments
- Remove unnecessary add_semiconj_by.eq
- Change prod.submonoid to submonoid.prod
- replacing a / at the end of docstring Sorry - don't make commits on your phone when your laptop's playing up :/
- removing some not very useful to_additives
- fix pi_instances namespaces
- remove unnecessary prefix
- change extensionality to ext not sure this is necessary because surely merging will change this automatically, but Travis told me to, and I really want it to compile, and I am not at my laptop