Theorem IsMulFreimanHom.to_isMulFreimanIso

Modification history

2026-05-18 11:49
Mathlib/Combinatorics/Additive/FreimanHom.lean
feat(Combinatorics/Additive): link Freiman homs and Freiman isos tighter (#38269)
Added IsMulFreimanHom.to_isMulFreimanIsoView on Github →