Commit 2026-05-18 11:49 34ff4236

View on Github →

feat(Combinatorics/Additive): link Freiman homs and Freiman isos tighter (#38269)

Estimated changes

Modified Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean

Modified Mathlib/Combinatorics/Additive/AP/Three/Defs.lean

Modified Mathlib/Combinatorics/Additive/FreimanHom.lean

added theorem IsMulFreimanHom.fst

modified theorem IsMulFreimanHom.mono

added theorem IsMulFreimanHom.prodMk

added theorem IsMulFreimanHom.prod_apply

added theorem IsMulFreimanHom.snd

added theorem IsMulFreimanHom.to_isMulFreimanIso

added theorem IsMulFreimanIso.symm

deleted theorem MonoidHomClass.isMulFreimanHom

added theorem MulHomClass.isMulFreimanHom

added theorem isMulFreimanHom_antitone