Mathlib Map

Theorems · Definition · ring theory

Pi.algHom

Deprecated since 2026-05-30Use AlgHom.pi instead.

{ι : Type u_1} →
  (R : Type u_2) →
    (A : ι → Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → Semiring (A i)] →
          [inst_2 : (i : ι) → Algebra R (A i)] →
            {B : Type u_4} →
              [inst_3 : Semiring B] → [inst_4 : Algebra R B] → ((i : ι) → B →ₐ[R] A i) → B →ₐ[R] (i : ι) → A i

Use AlgHom.pi instead.

Defined in
Mathlib.Algebra.Algebra.Pi
Cited by
2 results in Mathlib
Foundations
Depth 24 from the axioms · uses propext, Quot.sound
Assumes
CommSemiringSemiringAlgebraSemiringAlgebra
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Pi.algHom_apply · cited by 0Pi.algHom_applyPi.algHom_comp · cited by 0Pi.algHom_compSemiring · cited by 13802SemiringAlgebra · cited by 11388AlgebraCommSemiring · cited by 10911CommSemiringAlgHom · cited by 3236AlgHomAlgHom.pi · cited by 9AlgHom.piPi.algHomCITED BYCITES

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
  • AlgHomstatement and proof · cited by 3,236
  • AlgHom.piproof · cited by 9

Cited by2

Results whose statement or proof uses this declaration.