Theorems · Theorem · commutative algebra
IsAlgebraic.isIntegral
∀ {K : Type u} {A : Type v} [inst : Field K] [inst_1 : Ring A] [inst_2 : Algebra K A] {x : A},
IsAlgebraic K x → IsIntegral K xAlias of the forward direction of isAlgebraic_iff_isIntegral.
An element of an algebra over a field is algebraic if and only if it is integral.
- Defined in
- Mathlib.RingTheory.Algebraic.Integral
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 113 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Algebrastatement and proof · cited by 11,388
- Ringstatement and proof · cited by 7,463
- Fieldstatement and proof · cited by 7,404
- IsIntegralstatement · cited by 427
- IsAlgebraicstatement · cited by 163
- isAlgebraic_iff_isIntegralproof · cited by 12
Cited by25
Results whose statement or proof uses this declaration.
- minpoly.dvdproof · cited by 31
- minpoly.natSepDegree_eq_one_iff_pow_memproof · cited by 4
- IntermediateField.finSepDegree_adjoin_simple_eq_finrank_iffproof · cited by 4
- spectralNorm_uniqueproof · cited by 3
- RatFunc.transcendental_of_ne_Cproof · cited by 3
- spectralNorm_zero_ltproof · cited by 3
- isPowMul_spectralNormproof · cited by 3
- Polynomial.IsSplittingField.finiteDimensionalproof · cited by 3
- minpoly.eq_of_rootproof · cited by 2
- isIntegral_of_mem_solvableByRadproof · cited by 1
- minpoly.exists_algEquiv_of_rootproof · cited by 1
- IntermediateField.finSepDegree_adjoin_simple_le_finrankproof · cited by 1