Commit 2022-12-29 15:12 0690e5fb

View on Github →

chore: tidy various files (#1247)

Estimated changes

Modified Mathlib/Algebra/GroupPower/Lemmas.lean

Modified Mathlib/Algebra/GroupRingAction/Basic.lean

added theorem toRingHom_injective

deleted theorem to_ring_hom_injective

Modified Mathlib/Algebra/Hom/Aut.lean

Modified Mathlib/Algebra/Ring/Prod.lean

modified def RingEquiv.prodZeroRing

modified def RingEquiv.zeroRingProd

Modified Mathlib/Algebra/SMulWithZero.lean

modified def SMulWithZero.compHom

Modified Mathlib/Data/Int/Order/Basic.lean

Modified Mathlib/Data/Nat/Bits.lean

added theorem Nat.binaryRec_eq'

deleted theorem Nat.binary_rec_eq'

Modified Mathlib/Data/Nat/EvenOddRec.lean

Modified Mathlib/Data/Rat/Lemmas.lean

Modified Mathlib/Data/Set/Lattice.lean

Modified Mathlib/GroupTheory/Subsemigroup/Basic.lean

modified def MulHom.eqLocus

Modified Mathlib/Init/Data/Nat/Bitwise.lean

added theorem Nat.binaryRec_eq

added theorem Nat.binaryRec_zero

deleted theorem Nat.binary_rec_eq

deleted theorem Nat.binary_rec_zero

added theorem Nat.testBit_bitwise'

added theorem Nat.testBit_land'

added theorem Nat.testBit_ldiff'

added theorem Nat.testBit_lor'

added theorem Nat.testBit_lxor'

added theorem Nat.testBit_succ

added theorem Nat.testBit_zero

deleted theorem Nat.test_bit_bitwise'

deleted theorem Nat.test_bit_land'

deleted theorem Nat.test_bit_ldiff'

deleted theorem Nat.test_bit_lor'

deleted theorem Nat.test_bit_lxor'

deleted theorem Nat.test_bit_succ

deleted theorem Nat.test_bit_zero

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

added theorem WithTop.isGLB_infₛ'

added theorem WithTop.isGLB_infₛ

added theorem WithTop.isLUB_supₛ'

added theorem WithTop.isLUB_supₛ

deleted theorem WithTop.is_glb_infₛ'

deleted theorem WithTop.is_glb_infₛ

deleted theorem WithTop.is_lub_supₛ'

deleted theorem WithTop.is_lub_supₛ

deleted def conditionallyCompleteLatticeOfInf

added def conditionallyCompleteLatticeOfInfₛ

deleted def conditionallyCompleteLatticeOfLatticeOfInf

added def conditionallyCompleteLatticeOfLatticeOfInfₛ

deleted def conditionallyCompleteLatticeOfLatticeOfSup

added def conditionallyCompleteLatticeOfLatticeOfSupₛ

deleted def conditionallyCompleteLatticeOfSup

added def conditionallyCompleteLatticeOfSupₛ

added theorem isGLB_cinfᵢ

added theorem isGLB_cinfᵢ_set

added theorem isGLB_cinfₛ

added theorem isLUB_csupᵢ

added theorem isLUB_csupᵢ_set

added theorem isLUB_csupₛ'

added theorem isLUB_csupₛ

added theorem isLeast_cinfₛ

deleted theorem is_glb_cinfᵢ

deleted theorem is_glb_cinfᵢ_set

deleted theorem is_glb_cinfₛ

deleted theorem is_least_cinfₛ

deleted theorem is_lub_csupᵢ

deleted theorem is_lub_csupᵢ_set

deleted theorem is_lub_csupₛ'

deleted theorem is_lub_csupₛ

Modified Mathlib/Order/FixedPoints.lean

Modified Mathlib/Order/OrdContinuous.lean