Theorems · Definition · ring theory
TrivSqZeroExt.inrHom
(R : Type u) → (M : Type v) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → M →ₗ[R] TrivSqZeroExt R M
The canonical R-linear inclusion M → TrivSqZeroExt R M.
- Defined in
- Mathlib.Algebra.TrivSqZeroExt.Basic
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 26 from the axioms · uses propext, Quot.sound
- Assumes
- SemiringAddCommMonoidModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- RingHom.idstatement and proof · cited by 18,349
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- LinearMapstatement and proof · cited by 10,215
- TrivSqZeroExtstatement · cited by 180
- LinearMap.inrproof · cited by 62
- TrivSqZeroExt.inrproof · cited by 59
Cited by21
Results whose statement or proof uses this declaration.
- TrivSqZeroExt.mapproof · cited by 12
- ExteriorAlgebra.toTrivSqZeroExtproof · cited by 5
- ExteriorAlgebra.toTrivSqZeroExt_ιproof · cited by 4
- TrivSqZeroExt.map_inrproof · cited by 4
- TrivSqZeroExt.algHom_ext'statement and proof · cited by 3
- TrivSqZeroExt.inrHom_applystatement and proof · cited by 3
- CliffordAlgebraDualNumber.equivproof · cited by 2
- TensorAlgebra.toTrivSqZeroExtproof · cited by 2
- TensorAlgebra.ι_eq_algebraMap_iffproof · cited by 2
- TrivSqZeroExt.liftEquivproof · cited by 2
- TensorAlgebra.toTrivSqZeroExt_ιproof · cited by 1
- TrivSqZeroExt.snd_mapproof · cited by 1