Commit 2023-08-23 10:05 552f9b55

View on Github →

fix: simps config for Units (#6514)

Estimated changes

Modified Mathlib/Algebra/Algebra/Spectrum.lean

Modified Mathlib/Algebra/Group/Units.lean

added def Units.Simps.val_inv

Modified Mathlib/Algebra/Hom/Units.lean

added theorem IsUnit.val_inv_unit'

Modified Mathlib/Algebra/Invertible.lean

modified def Invertible.mulLeft

modified def Invertible.mulRight

modified def invertibleOfInvertibleMul

modified def invertibleOfMulInvertible

modified def unitOfInvertible

Modified Mathlib/Algebra/Lie/Classical.lean

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean

Modified Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

Modified Mathlib/Analysis/NormedSpace/Star/Spectrum.lean

Modified Mathlib/Analysis/NormedSpace/Units.lean

Modified Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup.lean

Modified Mathlib/NumberTheory/Cyclotomic/Gal.lean

Modified Mathlib/NumberTheory/Modular.lean

Modified Mathlib/NumberTheory/ModularForms/SlashActions.lean

Modified Mathlib/RingTheory/RootsOfUnity/Basic.lean