Commit 2023-08-01 19:57 6b9326b4

View on Github →

chore: tidy various files (#6274)

Estimated changes

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

deleted theorem OrderRingHom.coe_OrderAddMonoidHom_id

deleted theorem OrderRingHom.coe_OrderMonoidWithZeroHom_id

deleted theorem OrderRingHom.coe_RingHom_id

added theorem OrderRingHom.coe_orderAddMonoidHom_id

added theorem OrderRingHom.coe_orderMonoidWithZeroHom_id

added theorem OrderRingHom.coe_ringHom_id

Modified Mathlib/Combinatorics/Colex.lean

Modified Mathlib/Combinatorics/HalesJewett.lean

modified def Combinatorics.Line.diagonal

modified def Combinatorics.Line.horizontal

modified def Combinatorics.Line.map

modified def Combinatorics.Line.prod

modified def Combinatorics.Line.vertical

Modified Mathlib/Data/Nat/PartENat.lean

modified theorem PartENat.lt_coe_succ_iff_le

Modified Mathlib/FieldTheory/SplittingField/Construction.lean

Modified Mathlib/LinearAlgebra/Quotient.lean

modified def Submodule.comapMkQRelIso

Modified Mathlib/NumberTheory/Padics/PadicIntegers.lean

Modified Mathlib/Order/Category/FrmCat.lean

Modified Mathlib/Order/CompactlyGenerated.lean

Modified Mathlib/RingTheory/AdjoinRoot.lean

Modified Mathlib/Topology/Algebra/Order/MonotoneConvergence.lean