Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-05 17:58 21d4d1c2

View on Github →

feat(field_theory/perfect_closure): define the perfect closure of a field

Estimated changes

Modified data/nat/basic.lean

added theorem nat.iterate_cancel

added theorem nat.iterate_inj

added theorem nat.iterate₀

added theorem nat.iterate₁

added theorem nat.iterate₂

Created field_theory/perfect_closure.lean

added theorem frobenius_pth_root

added theorem is_ring_hom.pth_root

added def perfect_closure.UMP

added theorem perfect_closure.eq_iff'

added theorem perfect_closure.eq_iff

added theorem perfect_closure.eq_pth_root

added def perfect_closure.frobenius_equiv

added theorem perfect_closure.frobenius_equiv_apply

added theorem perfect_closure.frobenius_mk

added theorem perfect_closure.int_cast

added theorem perfect_closure.mk_zero

added theorem perfect_closure.nat_cast

added theorem perfect_closure.nat_cast_eq_iff

added def perfect_closure.of

added theorem perfect_closure.r.sound

added inductive perfect_closure.r

added def perfect_closure

added theorem pth_root_frobenius