Commit 2025-04-24 16:21 dffc5874

View on Github →

feat(Prod/Lex): prove Prod.Lex.covBy_iff (#24185) Also

move the definitions of CovBy and WCovBy to Defs/PartialOrder;
rename instances to use inst*;
golf a proof using aesop.

Estimated changes

Modified Mathlib/Algebra/Module/LinearMap/Defs.lean

Modified Mathlib/Algebra/Module/Submodule/Map.lean

Modified Mathlib/Data/Fin/FlagRange.lean

Modified Mathlib/Data/Prod/Lex.lean

added theorem Prod.Lex.covBy_iff

added theorem Prod.Lex.monotone_fst_ofLex

added theorem Prod.Lex.toLex_covBy_toLex_iff

Modified Mathlib/Order/Cover.lean

deleted def CovBy

deleted def WCovBy

Modified Mathlib/Order/Defs/PartialOrder.lean

added def CovBy

added def WCovBy