Mathlib Map

Structures · Algebra

VAdd

Type class for the +ᵥ notation.

Defined in
Mathlib.Algebra.Notation.Defs
Shape
2 explicit arguments · adds vadd
Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by2

Forgetful instances

Every VAdd is also a

Provided automatically by

Concrete types that are instances14

  • Quiver.Hom
  • Filter.Germ
  • DomAddAct
  • AddUnits
  • AddOreLocalization
  • Subtype
  • OrderDual
  • ULift
  • PUnit
  • Lex
  • AddOpposite
  • Colex
  • Additive
  • LinearMap

How is a type an instance?

Loading the hierarchy index…

Assumed by881

Ancestors1