Commit 2026-06-09 16:04 b70a2f6d

View on Github →

feat: use inferInstanceAs for algebraic Lex/Colex instances (#40049) This PR uses the new capabilities of inferInstanceAs to define the algebraic instances on Lex and Colex in a less leaky way, which lets us remove some backward.respectTransparency options.

Estimated changes

Modified Mathlib/Algebra/Field/Basic.lean

Modified Mathlib/Algebra/Order/Group/Action/Synonym.lean

Modified Mathlib/Algebra/Order/Group/Synonym.lean

Modified Mathlib/Algebra/Order/GroupWithZero/Action/Synonym.lean

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

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

Modified Mathlib/Algebra/Order/Module/HahnEmbedding.lean

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

deleted theorem ofLex_intCast

deleted theorem toLex_intCast

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

added theorem ofLex_intCast

added theorem ofLex_natCast

added theorem ofLex_ofNat

added theorem toLex_intCast

added theorem toLex_natCast

added theorem toLex_ofNat

Modified Mathlib/Data/Nat/Cast/Synonym.lean

deleted theorem ofLex_natCast

deleted theorem ofLex_ofNat

deleted theorem toLex_natCast

deleted theorem toLex_ofNat

Modified Mathlib/Order/Lex.lean

Modified Mathlib/RingTheory/HahnSeries/Lex.lean