Commit 2025-04-23 08:10 1652977a

View on Github →

chore: replace ring_inverse by ringInverse in lemma names (#24292) ... to follow the naming convention. From Toric

Estimated changes

Modified Mathlib/Algebra/Algebra/Spectrum/Basic.lean

Modified Mathlib/Algebra/GroupWithZero/Commute.lean

added theorem Commute.ringInverse_ringInverse

deleted theorem Commute.ring_inverse_ring_inverse

Modified Mathlib/Algebra/GroupWithZero/Units/Basic.lean

added theorem IsUnit.ringInverse

deleted theorem IsUnit.ring_inverse

deleted theorem Ring.IsUnit.ringInverse

added theorem isUnit_ringInverse

deleted theorem isUnit_ring_inverse

Modified Mathlib/Analysis/Calculus/ContDiff/Operations.lean

added theorem contDiffAt_ringInverse

deleted theorem contDiffAt_ring_inverse

Modified Mathlib/Analysis/Calculus/FDeriv/Mul.lean

added theorem hasFDerivAt_ringInverse

deleted theorem hasFDerivAt_ring_inverse

added theorem hasStrictFDerivAt_ringInverse

deleted theorem hasStrictFDerivAt_ring_inverse

Modified Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean

Modified Mathlib/Analysis/Normed/Algebra/Spectrum.lean

Modified Mathlib/Geometry/Manifold/Instances/UnitsOfNormedAlgebra.lean

Modified Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

added theorem Matrix.nonsing_inv_eq_ringInverse

deleted theorem Matrix.nonsing_inv_eq_ring_inverse

Modified Mathlib/LinearAlgebra/Matrix/SchurComplement.lean

Modified Mathlib/Topology/Algebra/Module/Equiv.lean

added theorem ContinuousLinearMap.inverse_eq_ringInverse

added theorem ContinuousLinearMap.ringInverse_eq_inverse

added theorem ContinuousLinearMap.ringInverse_equiv

deleted theorem ContinuousLinearMap.ring_inverse_eq_map_inverse

deleted theorem ContinuousLinearMap.ring_inverse_equiv

deleted theorem ContinuousLinearMap.to_ring_inverse