Theorem Algebra.IsAlgebraic.trans

Modification history

2025-02-11 17:21

Mathlib/RingTheory/Algebraic/Integral.lean

chore(RingTheory/Algebraic): remove unnecessary injectivity assumptions (#21566) …

Added Algebra.IsAlgebraic.trans View on Github →