Theorem AlgebraicIndependent.extendScalars_of_isSimpleRing

Modification history

2024-12-20 16:26
Mathlib/RingTheory/AlgebraicIndependent/AlgebraicClosure.lean
feat(RingTheory): `AlgebraicIndependent` persists to `algebraicClosure` (#19708) …
Added AlgebraicIndependent.extendScalars_of_isSimpleRingView on Github →