Mathlib.Algebra.GroupWithZero.NeZero

Module docstring

{"# 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. "}

NeZero.one instance

: NeZero (1 : M₀)

Full source

/-- In a nontrivial monoid with zero, zero and one are different. -/
instance NeZero.one : NeZero (1 : M₀) := ⟨by
  intro h
  rcases exists_pair_ne M₀ with ⟨x, y, hx⟩
  apply hx
  calc
    x = 1 * x := by rw [one_mul]
    _ = 0 := by rw [h, zero_mul]
    _ = 1 * y := by rw [h, zero_mul]
    _ = y := by rw [one_mul]⟩

Nonzero Identity in Nontrivial Monoid with Zero

Informal description

In a nontrivial monoid with zero, the multiplicative identity $1$ is different from the zero element $0$.

domain_nontrivial theorem

[Zero M₀'] [One M₀'] (f : M₀' → M₀) (zero : f 0 = 0) (one : f 1 = 1) : Nontrivial M₀'

Full source

/-- Pullback a `Nontrivial` instance along a function sending `0` to `0` and `1` to `1`. -/
theorem domain_nontrivial [Zero M₀'] [One M₀'] (f : M₀' → M₀) (zero : f 0 = 0) (one : f 1 = 1) :
    Nontrivial M₀' :=
  ⟨⟨0, 1, mt (congr_arg f) <| by
    rw [zero, one]
    exact zero_ne_one⟩⟩

Nontriviality Pullback via Zero-One Preserving Map

Informal description

Let $M₀'$ be a type with zero and one elements, and let $f : M₀' \to M₀$ be a function such that $f(0) = 0$ and $f(1) = 1$. If $M₀$ is a nontrivial monoid with zero, then $M₀'$ is also nontrivial.

inv_ne_zero theorem

(h : a ≠ 0) : a⁻¹ ≠ 0

Full source

theorem inv_ne_zero (h : a ≠ 0) : a⁻¹a⁻¹ ≠ 0 := fun a_eq_0 => by
  have := mul_inv_cancel₀ h
  simp only [a_eq_0, mul_zero, zero_ne_one] at this

Nonzero Elements Have Nonzero Inverses in a Group with Zero

Informal description

For any nonzero element $a$ in a group with zero, its multiplicative inverse $a^{-1}$ is also nonzero.

inv_mul_cancel₀ theorem

(h : a ≠ 0) : a⁻¹ * a = 1

Full source

@[simp]
theorem inv_mul_cancel₀ (h : a ≠ 0) : a⁻¹ * a = 1 :=
  calc
    a⁻¹ * a = a⁻¹ * a * a⁻¹ * a⁻¹a⁻¹⁻¹ := by simp [inv_ne_zero h]
    _ = a⁻¹ * a⁻¹a⁻¹⁻¹ := by simp [h]
    _ = 1 := by simp [inv_ne_zero h]

Left Cancellation Property for Nonzero Elements in a Group with Zero

Informal description

For any nonzero element $a$ in a group with zero $G_0$, the product of its multiplicative inverse $a^{-1}$ and $a$ equals the multiplicative identity, i.e., $a^{-1} \cdot a = 1$.