Commit 2024-12-20 11:33 7c2ef337

View on Github →

chore(IsAlgClosed/Classification): make theorems more universe polymorphic (#18434)

Estimated changes

Modified Mathlib/FieldTheory/IsAlgClosed/Classification.lean

added theorem IsAlgClosed.cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt'

added theorem IsAlgClosed.cardinal_le_max_transcendence_basis'

deleted theorem IsAlgClosed.ringEquivOfCardinalEqOfCharEq

deleted theorem IsAlgClosed.ringEquivOfCardinalEqOfCharZero

added theorem IsAlgClosed.ringEquiv_of_equiv_of_charZero

added theorem IsAlgClosed.ringEquiv_of_equiv_of_char_eq

Modified Mathlib/ModelTheory/Algebra/Field/IsAlgClosed.lean

modified theorem FirstOrder.Field.ACF_categorical