Commit 2023-04-12 19:26 35a20e11

View on Github →

feat: irreducible_def: support protected, equation lemmas (#3395)

Estimated changes

Modified Mathlib/GroupTheory/MonoidLocalization.lean

modified theorem Localization.mk_mul

modified theorem Localization.mk_one

modified theorem Localization.mk_pow

Modified Mathlib/RingTheory/Localization/Basic.lean

Modified Mathlib/RingTheory/Localization/FractionRing.lean

Modified Mathlib/Tactic/Eqns.lean

Modified Mathlib/Tactic/IrreducibleDef.lean

added def Lean.Elab.Command.$n:ident$[.{$us,*}]?

deleted theorem Lean.Elab.Command.$n_def:ident

deleted structure Lean.Elab.Command.Wrapper$[.{$us,*}]?

deleted def Lean.Elab.Command.definition$[.{$us,*}]?

Modified test/irreducibleDef.lean