Documentation

Mathlib.Algebra.Module.MinimalAxioms

Minimal Axioms for a Module #

This file defines a constructor to define a Module structure on a Type with an AddCommGroup, while proving a minimum number of equalities.

Main Definitions #

@[reducible, inline]
abbrev Module.ofMinimalAxioms {R : Type u} {M : Type v} [Semiring R] [AddCommGroup M] [SMul R M] (smul_add : ∀ (r : R) (x y : M), r (x + y) = r x + r y) (add_smul : ∀ (r s : R) (x : M), (r + s) x = r x + s x) (mul_smul : ∀ (r s : R) (x : M), (r * s) x = r s x) (one_smul : ∀ (x : M), 1 x = x) :
Module R M

Define a Module structure on a Type by proving a minimized set of axioms.

Equations
Instances For