Mathlib Map

Structures · Lean core

Lean.Grind.IntModule

A module over the integers, i.e. a type with zero, addition, negation, subtraction, and scalar multiplication by integers, satisfying appropriate compatibilities. Equivalently, an additive commutative group.

Defined in
Init.Grind.Module.Basic
Shape
One type argument · adds nsmul, zsmul, zero_zsmul, one_zsmul, add_zsmul, zsmul_natCast_eq_nsmul
Open in Mathlib docs

Extends1

Extended by2

Forgetful instances

Every Lean.Grind.IntModule is also a

Provided automatically by

Concrete types that are instances2

  • Vector
  • Lean.Grind.IntModule.OfNatModule.Q

How is a type an instance?

Loading the hierarchy index…

Assumed by0

No theorem or definition in Mathlib takes this class as a hypothesis.

Ancestors14