Theorem coe_frobenius_comp_coe_frobeniusEquiv_symm

Modification history

2025-11-11 15:04
Mathlib/FieldTheory/Perfect.lean
feat(RingTheory/Perfection): lemmas for `frobeniusEquiv.symm` (#26386) …
Added coe_frobenius_comp_coe_frobeniusEquiv_symmView on Github →