Theorems · Definition
HVAdd.hVAdd
{α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HVAdd α β γ] → α → β → γa +ᵥ b computes the sum of a and b.
The meaning of this notation is type-dependent.
Conventions for notations in identifiers:
* The recommended spelling of +ᵥ in identifiers is vadd.
- Defined in
- Mathlib.Algebra.Notation.Defs
- Cited by
- 1,820 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 3 definitions · uses no axioms
- Assumes
- HVAdd
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.
- HVAddstatement and proof · cited by 9
Cited by2,025
Results whose statement or proof uses this declaration.
- Set.vaddSetproof · cited by 403
- AffineMap.lineMapproof · cited by 254
- Finset.affineCombinationproof · cited by 159
- zero_vaddstatement · cited by 95
- neg_vsub_eq_vsub_revproof · cited by 87
- AddAction.orbitproof · cited by 86
- Set.vaddproof · cited by 72
- Finset.vaddFinsetproof · cited by 70
- AddAction.IsBlockproof · cited by 65
- vsub_vaddstatement · cited by 62
- vadd_vsubstatement · cited by 58
- AffineMap.homothetyproof · cited by 51
Showing the 200 most cited of 2,025.