Theorems · Theorem · commutative algebra

Algebra.Presentation.HasCoeffs.coeffs_subset_range

∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} {inst : CommRing R} {inst_1 : CommRing S}
  {inst_2 : Algebra R S} {P : Algebra.Presentation R S ι σ} {R₀ : Type u_5} {inst_3 : CommRing R₀}
  {inst_4 : Algebra R₀ R} {inst_5 : Algebra R₀ S} {inst_6 : IsScalarTower R₀ R S} [self : P.HasCoeffs R₀],
  P.coeffs ⊆ Set.range ⇑(algebraMap R₀ R)

Defined in

Mathlib.RingTheory.Extension.Presentation.Core

Cited by

2 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Algebra.Presentation.HasCoeffs