Commit 2025-02-19 16:57 31681c96

View on Github →

chore(Order/GaloisConnection/Defs): don't import OrderIso (#22044) There's a more natural place for those lemmas anyway.

Estimated changes

Modified Mathlib/Algebra/Field/Opposite.lean

Modified Mathlib/Algebra/Group/Center.lean

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

Modified Mathlib/Algebra/Group/Subgroup/Even.lean

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

Modified Mathlib/Algebra/Group/Submonoid/DistribMulAction.lean

Modified Mathlib/Algebra/Group/Submonoid/MulAction.lean

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

Modified Mathlib/Algebra/GroupWithZero/Action/End.lean

Modified Mathlib/Algebra/GroupWithZero/Center.lean

Modified Mathlib/Algebra/GroupWithZero/Submonoid.lean

Modified Mathlib/Algebra/Module/End.lean

Modified Mathlib/Algebra/Module/NatInt.lean

Modified Mathlib/Algebra/NoZeroSMulDivisors/Defs.lean

Modified Mathlib/Algebra/Order/GroupWithZero/Submonoid.lean

Modified Mathlib/Algebra/Order/Interval/Set/Instances.lean

Modified Mathlib/Algebra/Ring/Action/Invariant.lean

Modified Mathlib/Algebra/Ring/Action/Subobjects.lean

Modified Mathlib/Algebra/Ring/Center.lean

Modified Mathlib/Algebra/Ring/Centralizer.lean

Modified Mathlib/Algebra/Ring/Hom/Basic.lean

Modified Mathlib/Algebra/Ring/Subring/Defs.lean

Modified Mathlib/Algebra/Ring/Subsemiring/Defs.lean

Modified Mathlib/Data/Bundle.lean

Modified Mathlib/Data/Int/Cast/Lemmas.lean

Modified Mathlib/Data/Nat/Order/Lemmas.lean

Modified Mathlib/Data/PEquiv.lean

Modified Mathlib/Data/Part.lean

Modified Mathlib/Data/Set/Basic.lean

Modified Mathlib/Data/Set/BoolIndicator.lean

Modified Mathlib/Data/Set/Enumerate.lean

Modified Mathlib/Data/Set/Image.lean

Modified Mathlib/Data/Set/Subsingleton.lean

Modified Mathlib/Data/Set/SymmDiff.lean

Modified Mathlib/Data/SetLike/Basic.lean

Modified Mathlib/GroupTheory/OreLocalization/Basic.lean

Modified Mathlib/GroupTheory/OreLocalization/OreSet.lean

Modified Mathlib/GroupTheory/Subsemigroup/Center.lean

Modified Mathlib/Logic/Function/FiberPartition.lean

Modified Mathlib/Order/BooleanAlgebra.lean

Modified Mathlib/Order/Bounded.lean

Modified Mathlib/Order/Circular.lean

Modified Mathlib/Order/Cofinal.lean

Modified Mathlib/Order/Filter/Defs.lean

Modified Mathlib/Order/GaloisConnection/Basic.lean

added theorem OrderIso.to_galoisConnection

Modified Mathlib/Order/GaloisConnection/Defs.lean

deleted theorem OrderIso.to_galoisConnection

Modified Mathlib/Order/Heyting/Basic.lean

Modified Mathlib/Order/Heyting/Boundary.lean

Modified Mathlib/Order/Interval/Set/Basic.lean

Modified Mathlib/Order/SymmDiff.lean

Modified Mathlib/RingTheory/NonUnitalSubring/Defs.lean

Modified Mathlib/RingTheory/NonUnitalSubsemiring/Defs.lean

Modified Mathlib/RingTheory/OreLocalization/Basic.lean

Modified Mathlib/RingTheory/OreLocalization/OreSet.lean

Modified Mathlib/Tactic/NormNum/Pow.lean

Modified Mathlib/Tactic/NormNum/PowMod.lean

Modified Mathlib/Tactic/TautoSet.lean