Theorems · Theorem · ring theory
NonUnitalRingHom.pi_injective
∀ {I : Type u} {f : I → Type u_1} {γ : Type u_2} [Nonempty I] [inst : (i : I) → NonUnitalNonAssocSemiring (f i)]
[inst_1 : NonUnitalNonAssocSemiring γ] (g : (i : I) → γ →ₙ+* f i),
(∀ (i : I), Function.Injective ⇑(g i)) → Function.Injective ⇑(NonUnitalRingHom.pi g)- Defined in
- Mathlib.Algebra.Ring.Pi
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- NonUnitalNonAssocSemiringstatement and proof · cited by 1,081
- NonUnitalRingHomstatement and proof · cited by 157
- NonUnitalRingHom.toMulHomproof · cited by 15
- NonUnitalRingHom.pistatement · cited by 4
- MulHom.pi_injectiveproof · cited by 4
Cited by1
Results whose statement or proof uses this declaration.
- Pi.nonUnitalRingHom_injectiveproof · cited by 0