Theorems · Definition · ring theory

AlgEquiv.sumArrowEquivProdArrow

(α : Type u_1) →
  (β : Type u_2) →
    (R : Type u_3) →
      [inst : CommSemiring R] →
        (S : Type u_8) → [inst_1 : Semiring S] → [inst_2 : Algebra R S] → (α ⊕ β → S) ≃ₐ[R] (α → S) × (β → S)

Equiv.sumArrowEquivProdArrow as an algebra equivalence.

Defined in: Mathlib.Algebra.Algebra.Pi
Cited by: 3 results in Mathlib
Foundations: Depth 23 from the axioms · uses propext, Quot.sound
Assumes: CommSemiring Semiring Algebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Semiringstatement and proof · cited by 13,802
Algebrastatement and proof · cited by 11,388
CommSemiringstatement and proof · cited by 10,911
AlgEquivstatement · cited by 1,681
AlgEquiv.ofRingEquivproof · cited by 12

Cited by3

Results whose statement or proof uses this declaration.

AlgEquiv.sumArrowEquivProdArrow_applystatement · cited by 0
AlgEquiv.sumArrowEquivProdArrow_symm_apply_inrstatement · cited by 0
Algebra.IsFiniteSplit.exists_tensorProduct_of_etaleproof · cited by 0