Theorem Algebra.IsAlgebraic.injective_tower_top

Modification history

2025-02-11 17:21

Mathlib/RingTheory/Algebraic/Basic.lean

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

Added Algebra.IsAlgebraic.injective_tower_top View on Github →