Documentation

Mathlib.Algebra.GroupWithZero.NeZero

NeZero 1 in a nontrivial MulZeroOneClass. #

This file exists to minimize the dependencies of Mathlib.Algebra.GroupWithZero.Defs, which is a part of the algebraic hierarchy used by basic tactics.

instance NeZero.one {M₀ : Type u_1} [MulZeroOneClass M₀] [Nontrivial M₀] :

In a nontrivial monoid with zero, zero and one are different.

Equations
  • =
theorem pullback_nonzero {M₀ : Type u_1} {M₀' : Type u_2} [MulZeroOneClass M₀] [Nontrivial M₀] [Zero M₀'] [One M₀'] (f : M₀'M₀) (zero : f 0 = 0) (one : f 1 = 1) :

Pullback a Nontrivial instance along a function sending 0 to 0 and 1 to 1.

theorem inv_ne_zero {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} (h : a 0) :
@[simp]
theorem inv_mul_cancel₀ {G₀ : Type u_3} [GroupWithZero G₀] {a : G₀} (h : a 0) :
a⁻¹ * a = 1