Commit 2020-04-03 12:34 a590d4b5
View on Github →feat(group_theory/monoid_localization): some homs induced on localizations: lift, map (#2118)
- should I be changing and committing toml idk
- initial monoid loc lemmas
- responding to PR comments
- removing bad @[simp]
- inhabited instances
- remove #lint
- additive inhabited instance
- using is_unit & is_add_unit
- doc string
- remove simp
- submonoid.monoid_loc... -> submonoid.localization
- submonoid.monoid_loc... -> submonoid.localization
- generalize inhabited instance
- remove inhabited instance
- 2nd section
- docs and linting
- removing questionable
@[simp]s - removing away
- adding lemmas, removing 'include'
- removing import
- responding to PR comments
- use eq_of_eq to prove comp_eq_of_eq
- name change
- trying to update mathlib
- make lemma names consistent
- Update src/algebra/group/is_unit.lean
- Update src/algebra/group/is_unit.lean
- fix build
- documentation and minor changes
- spacing
- fix build
- applying comments