Theorem Algebra.IsAlgebraic.isAlgebraic_iff_bot

Modification history

2025-04-24 04:08
Mathlib/RingTheory/Algebraic/Integral.lean
chore(RingTheory): equivalence between algebraicity over `IntermediateField.adjoin` and `Algebra.adjoin` (#24004)
Added Algebra.IsAlgebraic.isAlgebraic_iff_botView on Github →