Theorems · Theorem · commutative algebra

Algebra.FormallyUnramified.finite_of_free_aux

∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (I : Type u_4)
  [inst_3 : DecidableEq I] (b : Module.Basis I R S) (f : I →₀ S) (x : S) (a : I → I →₀ R),
  (a = fun i => b.repr (b i * x)) →
    (1 ⊗ₜ[R] x * f.sum fun i y => y ⊗ₜ[R] b i) =
      ∑ k ∈ f.support.biUnion fun i => (a i).support,
        (b.repr (f.sum fun i y => (a i) k • y)).sum fun j c => c • b j ⊗ₜ[R] b k

Defined in

Mathlib.RingTheory.Unramified.Finite

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraDecidableEq