Theorem Localization.liftOn_mk'

Modification history

2023-12-21 20:35

Mathlib/GroupTheory/MonoidLocalization.lean

chore(*): use `∃ x ∈ s, _` instead of `∃ (x) (_ : x ∈ s), _` (#9184) …

Modified Localization.liftOn_mk'View on Github →

2023-01-30 10:29

Mathlib/GroupTheory/MonoidLocalization.lean

feat: port GroupTheory.Monoid.Localization (#1777)

Added Localization.liftOn_mk'View on Github →