Theorem MvPolynomial.isAlgebraic_of_mem_vars_of_forall_totalDegree_le

Modification history

2025-12-05 11:03
Mathlib/FieldTheory/SeparablyGenerated.lean
feat(FieldTheory): fg extension over perfect field is separably generated (#30998)
Added MvPolynomial.isAlgebraic_of_mem_vars_of_forall_totalDegree_leView on Github →