Theorems · Definition · commutative algebra

PiTensorProduct.constantBaseRingEquiv

(ι : Type u_1) → (R : Type u_3) → [inst : CommSemiring R] → [Fintype ι] → (PiTensorProduct R fun x => R) ≃ₐ[R] R

The algebra equivalence from the tensor product of the constant family with value R to R, given by multiplication of the entries.

Defined in

Mathlib.RingTheory.PiTensorProduct

Cited by

7 results in Mathlib

Foundations

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

Assumes

CommSemiringFintype