Commit 2023-06-10 04:50 71f13844

View on Github →

feat: port FieldTheory.IsAlgClosed.Classification (#4940)

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/IsAlgClosed/Classification.lean

added theorem Algebra.IsAlgebraic.cardinal_mk_le_max

added theorem Algebra.IsAlgebraic.cardinal_mk_le_sigma_polynomial

added theorem IsAlgClosed.cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt

added theorem IsAlgClosed.cardinal_le_max_transcendence_basis

added def IsAlgClosed.equivOfTranscendenceBasis

added theorem IsAlgClosed.isAlgClosure_of_transcendence_basis

added theorem IsAlgClosed.ringEquivOfCardinalEqOfCharEq

added theorem IsAlgClosed.ringEquivOfCardinalEqOfCharZero