Theorems · Theorem · ring theory

Pi.nonUnitalRingHom_apply

Deprecated since 2026-05-30Use NonUnitalRingHom.pi_apply instead.

∀ {I : Type u} {f : I → Type u_1} {γ : Type u_2} [inst : (i : I) → NonUnitalNonAssocSemiring (f i)]
  [inst_1 : NonUnitalNonAssocSemiring γ] (g : (i : I) → γ →ₙ+* f i) (x : γ) (b : I),
  (NonUnitalRingHom.pi g) x b = (g b) x

Alias of NonUnitalRingHom.pi_apply.

Defined in

Mathlib.Algebra.Ring.Pi

Cited by

0 results in Mathlib

Foundations

Depth 17 from the axioms · uses Quot.sound

Assumes

NonUnitalNonAssocSemiringNonUnitalNonAssocSemiring