Theorem Transcendental.extendScalars_of_isIntegral

Modification history

2025-04-24 04:08
Mathlib/RingTheory/Algebraic/Integral.lean
chore(RingTheory): equivalence between algebraicity over `IntermediateField.adjoin` and `Algebra.adjoin` (#24004)
Modified Transcendental.extendScalars_of_isIntegralView on Github →
2025-02-11 17:21
Mathlib/RingTheory/Algebraic/Integral.lean
chore(RingTheory/Algebraic): remove unnecessary injectivity assumptions (#21566) …
Modified Transcendental.extendScalars_of_isIntegralView on Github →
2024-12-05 08:47
Mathlib/RingTheory/Algebraic/Integral.lean
feat(RingTheory/Algebraic): transitivity of algebraicity (#19660) …
Added Transcendental.extendScalars_of_isIntegralView on Github →