Theorems · Theorem · commutative algebra

Algebra.Presentation.finite_coeffs

∀ {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 ι σ} [Finite σ], P.coeffs.Finite

Defined in

Mathlib.RingTheory.Extension.Presentation.Core

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraFinite