Theorems · Inductive type · group theory

SMulWithZero

(M₀ : Type u_2) → (A : Type u_7) → [Zero M₀] → [Zero A] → Type (max u_2 u_7)

SMulWithZero is a class consisting of a Type M₀ with 0 ∈ M₀ and a scalar multiplication of M₀ on a Type A with 0, such that the equality r • m = 0 holds if at least one among r or m equals 0.

Defined in

Mathlib.Algebra.GroupWithZero.Action.Defs

Cited by

113 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

ZeroZero