Commit 2024-07-15 08:59 bd8361bb

View on Github →

feat(RingTheory/Algebraic): define Algebra.Transcendental and some lemmas (#14710) Define Algebra.Transcendental, analogous to Algebra.IsAlgebraic, and some lemmas. Also prove transcendental_iff_injective, a negated version of isAlgebraic_iff_not_injective.

Estimated changes

Modified Mathlib/RingTheory/Algebraic.lean

added theorem Algebra.transcendental_def

added theorem Algebra.transcendental_iff_not_isAlgebraic

added theorem transcendental_iff_injective