Theorems · Theorem · commutative algebra
Algebra.adjoin_singleton_eq_range_aeval
∀ (R : Type u) {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A),
R[x] = (Polynomial.aeval x).range- Cited by
- 12 results in Mathlib
- Foundations
- Depth 111 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommSemiringSemiringAlgebra
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Semiringstatement and proof · cited by 13,802
- Algebrastatement and proof · cited by 11,388
- CommSemiringstatement and proof · cited by 10,911
- Polynomialstatement and proof · cited by 5,681
- Polynomial.Xproof · cited by 1,639
- Subalgebrastatement and proof · cited by 1,353
- Polynomial.aevalstatement and proof · cited by 615
- Algebra.adjoinstatement and proof · cited by 535
- Set.image_singletonproof · cited by 174
- AlgHom.rangestatement · cited by 169
- Polynomial.aeval_Xproof · cited by 120
Cited by12
Results whose statement or proof uses this declaration.
- Polynomial.aeval_mem_adjoin_singletonproof · cited by 7
- Algebra.adjoin_eq_exists_aevalproof · cited by 4
- AdjoinRoot.adjoinRoot_eq_topproof · cited by 4
- Submodule.span_range_natDegree_eq_adjoinproof · cited by 3
- IsLocalRing.adjoin_residue_eq_top_iff_adjoin_eq_topproof · cited by 2
- IntermediateField.mem_adjoin_simple_iffproof · cited by 2
- Module.End.IsSemisimple.of_mem_adjoin_singletonproof · cited by 1
- Algebra.TensorProduct.not_isField_of_transcendentalproof · cited by 1
- mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAtproof · cited by 1
- IsAdjoinRoot.adjoin_root_eq_topproof · cited by 1
- Algebra.adjoin_mem_exists_aevalproof · cited by 0
- IsPrimitiveRoot.powerBasis_gen_mem_adjoin_zeta_sub_oneproof · cited by 0