Theorems · Definition · ring theory
Unitization.inl
{R : Type u_1} → {A : Type u_2} → [Zero A] → R → Unitization R AThe canonical inclusion R → Unitization R A.
- Defined in
- Mathlib.Algebra.Algebra.Unitization
- Cited by
- 27 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
- Assumes
- Zero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Unitizationstatement · cited by 220
Cited by28
Results whose statement or proof uses this declaration.
- Unitization.indstatement and proof · cited by 6
- Unitization.inlRingHomproof · cited by 3
- AlgHomClass.unitization_injective'proof · cited by 1
- Unitization.splitMul_injective_of_clm_mul_injectiveproof · cited by 1
- Unitization.starLift_range_leproof · cited by 1
- Unitization.lift_range_leproof · cited by 1
- Unitization.linearMap_extstatement and proof · cited by 1
- Unitization.fst_inlstatement · cited by 1
- Unitization.inl_fst_add_inr_snd_eqstatement · cited by 1
- Unitization.inl_injectivestatement · cited by 1
- Unitization.inl_mulstatement · cited by 1
- Unitization.inl_mul_inlstatement · cited by 0