Theorems · Theorem · commutative algebra

Algebra.SubmersivePresentation.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} {inst_3 : Finite σ} {P : Algebra.SubmersivePresentation R S ι σ} {R₀ : Type u_5}
  {inst_4 : CommRing R₀} {inst_5 : Algebra R₀ R} {inst_6 : Algebra R₀ S} {inst_7 : IsScalarTower R₀ R S}
  [self : P.HasCoeffs R₀], P.coeffs ⊆ ↑(algebraMap R₀ R).range

Defined in

Mathlib.RingTheory.Extension.Presentation.Core

Cited by

2 results in Mathlib

Foundations

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

Assumes

Algebra.SubmersivePresentation.HasCoeffs