Commit 2025-11-12 10:34 e7c94378

View on Github →

chore: rename isUnit_of_mul_eq_one to IsUnit.of_mul_eq_one (#31283) ... to leverage anonymous dot notation.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Associated.lean

Modified Mathlib/Algebra/CharP/CharAndCard.lean

Modified Mathlib/Algebra/Field/Equiv.lean

Modified Mathlib/Algebra/Group/Int/Units.lean

Modified Mathlib/Algebra/Group/Units/Defs.lean

added theorem IsUnit.of_mul_eq_one

added theorem IsUnit.of_mul_eq_one_right

deleted theorem isUnit_of_mul_eq_one

deleted theorem isUnit_of_mul_eq_one_right

Modified Mathlib/Algebra/GroupWithZero/Associated.lean

Modified Mathlib/Algebra/Polynomial/Eval/Irreducible.lean

Modified Mathlib/Algebra/Polynomial/FieldDivision.lean

Modified Mathlib/Algebra/Polynomial/Monic.lean

Modified Mathlib/AlgebraicGeometry/EllipticCurve/ModelsWithJ.lean

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

Modified Mathlib/AlgebraicGeometry/StructureSheaf.lean

Modified Mathlib/Data/Nat/Factorial/NatCast.lean

Modified Mathlib/Geometry/RingedSpace/Basic.lean

Modified Mathlib/GroupTheory/MonoidLocalization/Away.lean

Modified Mathlib/LinearAlgebra/Determinant.lean

Modified Mathlib/LinearAlgebra/JordanChevalley.lean

Modified Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

Modified Mathlib/LinearAlgebra/RootSystem/Base.lean

Modified Mathlib/NumberTheory/LucasLehmer.lean

Modified Mathlib/NumberTheory/Pell.lean

Modified Mathlib/RingTheory/Coprime/Basic.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal/Basic.lean

Modified Mathlib/RingTheory/DedekindDomain/PID.lean

Modified Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean

Modified Mathlib/RingTheory/HahnSeries/Summable.lean

Modified Mathlib/RingTheory/Ideal/Quotient/Nilpotent.lean

Modified Mathlib/RingTheory/Ideal/Quotient/PowTransition.lean

Modified Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean

Modified Mathlib/RingTheory/Jacobson/Ideal.lean

Modified Mathlib/RingTheory/Localization/Away/AdjoinRoot.lean

Modified Mathlib/RingTheory/Multiplicity.lean

Modified Mathlib/RingTheory/MvPowerSeries/Inverse.lean

Modified Mathlib/RingTheory/Polynomial/Content.lean

Modified Mathlib/RingTheory/Polynomial/Nilpotent.lean

Modified Mathlib/RingTheory/PowerSeries/WeierstrassPreparation.lean

Modified Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean

modified theorem IsPrimitiveRoot.isUnit

Modified Mathlib/RingTheory/Trace/Basic.lean

Modified Mathlib/RingTheory/Valuation/ValuationRing.lean

Modified Mathlib/RingTheory/Valuation/ValuationSubring.lean

modified theorem ValuationSubring.valuation_eq_one_iff