Commit 2024-11-13 11:57 c13f1a03

View on Github →

chore: generalize {Mul, Add}EquivClass.map_{eq, ne}_one_iff (#18809)

Estimated changes

Modified Mathlib/Algebra/Group/Equiv/Basic.lean

added theorem EmbeddingLike.map_eq_one_iff

added theorem EmbeddingLike.map_ne_one_iff

deleted theorem MulEquivClass.map_eq_one_iff

deleted theorem MulEquivClass.map_ne_one_iff

Modified Mathlib/Algebra/MvPolynomial/Equiv.lean

Modified Mathlib/Algebra/Polynomial/AlgebraMap.lean

Modified Mathlib/Algebra/Ring/Equiv.lean

Modified Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

Modified Mathlib/FieldTheory/SplittingField/Construction.lean

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

Modified Mathlib/RingTheory/Flat/Basic.lean

Modified Mathlib/RingTheory/HahnSeries/Addition.lean

Modified Mathlib/RingTheory/Polynomial/Opposites.lean

Modified Mathlib/RingTheory/RootsOfUnity/Basic.lean