Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-26 09:47 add100aa

View on Github →

feat(ring_theory/perfection): perfection.map (#5503)

Estimated changes

Modified src/ring_theory/perfection.lean

added theorem perfection.coeff_map

added theorem perfection.coeff_pow_p'

added theorem perfection.hom_ext

added def perfection.map

added theorem perfection_map.comp_equiv'

added theorem perfection_map.comp_equiv

added theorem perfection_map.comp_map

added theorem perfection_map.comp_symm_equiv'

added theorem perfection_map.comp_symm_equiv

added theorem perfection_map.equiv_apply

added theorem perfection_map.hom_ext

added theorem perfection_map.map_eq_map

added theorem perfection_map.map_map