Theorems · Theorem · commutative algebra

Ideal.basisSpanSingleton_apply

∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra R S] (b : Module.Basis ι R S) {x : S} (hx : x ≠ 0) (i : ι),
  ↑((Ideal.basisSpanSingleton b hx) i) = x * b i

Defined in

Mathlib.RingTheory.Ideal.Basis

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringCommRingIsDomainAlgebra