Theorems · Theorem · group theory

AddCon.map_of_add_left_rel_zero

∀ {M : Type u_1} [inst : AddMonoid M] (c : AddCon M) (f : M → M),
  (∀ (x : M), c (f x + x) 0) → ∀ {x y : M}, c x y → c (f x) (f y)

Sometimes, an additive group is defined as a quotient of a monoid by an additive congruence relation. Usually, the inverse operation is defined as Setoid.map f _ for some f. This lemma allows to avoid code duplication in the definition of the inverse operation: instead of proving both ∀ x y, c x y → c (f x) (f y) (to define the operation) and ∀ x, c (f x + x) 0 (to prove the group laws), one can only prove the latter.

Defined in

Mathlib.GroupTheory.Congruence.Defs

Cited by

1 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Quot.sound

Assumes

AddMonoid