Def AlgebraicIndepOn.aevalEquiv

Modification history

2025-12-05 11:03
Mathlib/RingTheory/AlgebraicIndependent/Defs.lean
feat(FieldTheory): fg extension over perfect field is separably generated (#30998)
Added AlgebraicIndepOn.aevalEquivView on Github →