Documentation

Mathlib.Algebra.GroupWithZero.NeZero

NeZero 1 in a nontrivial MulZeroOneClass. #

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

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

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

source
theorem domain_nontrivial {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) :
Nontrivial M₀'

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

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