Commit 2025-06-18 19:56 4de2caee
View on Github →chore(Submodule): deprecate a duplicated lemma (#26116)
The lemma LinearEquiv.map_eq_comap can be immediately proved from Submodule.map_equiv_eq_comap_symm, so we deprecate the former.
chore(Submodule): deprecate a duplicated lemma (#26116)
The lemma LinearEquiv.map_eq_comap can be immediately proved from Submodule.map_equiv_eq_comap_symm, so we deprecate the former.