Theorems · Definition
VAdd.vadd
{G : Type u} → {P : Type v} → [self : VAdd G P] → G → P → Pa +ᵥ b computes the sum of a and b. The meaning of this notation is type-dependent,
but it is intended to be used for left actions.
- Defined in
- Mathlib.Algebra.Notation.Defs
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- VAdd
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.
- VAddstatement and proof · cited by 616
Cited by11
Results whose statement or proof uses this declaration.
- VAdd.extstatement and proof · cited by 1
- AddSemigroupAction.extstatement and proof · cited by 1
- AddAction.extstatement and proof · cited by 1
- AddDistribAddAction.extstatement and proof · cited by 1
- Set.vadd_set_univ_piproof · cited by 0
- VAdd.ext_iffstatement and proof · cited by 0
- vadd_univ_piproof · cited by 0
- arrowAddAction_vaddstatement and proof · cited by 0
- AddSemigroupAction.ext_iffstatement and proof · cited by 0
- AddAction.ext_iffstatement and proof · cited by 0
- AddDistribAddAction.ext_iffstatement and proof · cited by 0