Theorem IsAlgebraic.exists_integral_multiple

Modification history

2025-02-11 17:21

Mathlib/RingTheory/Algebraic/Integral.lean

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

Modified IsAlgebraic.exists_integral_multiple View on Github →

2024-12-05 08:47

Mathlib/RingTheory/Algebraic/Integral.lean

feat(RingTheory/Algebraic): transitivity of algebraicity (#19660) …

Added IsAlgebraic.exists_integral_multiple View on Github →