Mathlib Changelog
v4
Changelog
About
Github
Theorem
coe_frobeniusEquiv_symm_comp_coe_frobenius
Modification history
2025-11-11 15:04
Mathlib/FieldTheory/Perfect.lean
feat(RingTheory/Perfection): lemmas for `frobeniusEquiv.symm` (#26386) …
Added
coe_frobeniusEquiv_symm_comp_coe_frobenius
View on Github →