Documentation

Mathlib.Algebra.Ring.Ext

Extensionality lemmas for rings and similar structures #

In this file we prove extensionality lemmas for the ring-like structures defined in Mathlib/Algebra/Ring/Defs.lean, ranging from NonUnitalNonAssocSemiring to CommRing. These extensionality lemmas take the form of asserting that two algebraic structures on a type are equal whenever the addition and multiplication defined by them are both the same.

Implementation details #

We follow Mathlib/Algebra/Group/Ext.lean in using the term (letI := i; HMul.hMul : R → R → R) to refer to the multiplication specified by a typeclass instance i on a type R (and similarly for addition). We abbreviate these using some local notations.

Since Mathlib/Algebra/Group/Ext.lean proved several injectivity lemmas, we do so as well — even if sometimes we don't need them to prove extensionality.

Tags #

semiring, ring, extensionality

Distrib #

theorem Distrib.ext {R : Type u} ⦃inst₁ inst₂ : Distrib R⦄ (h_add : HAdd.hAdd = HAdd.hAdd) (h_mul : HMul.hMul = HMul.hMul) :

inst₁ = inst₂

theorem Distrib.ext_iff {R : Type u} {inst₁ inst₂ : Distrib R} :

inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul

NonUnitalNonAssocSemiring #

theorem NonUnitalNonAssocSemiring.ext {R : Type u} ⦃inst₁ inst₂ : NonUnitalNonAssocSemiring R⦄ (h_add : HAdd.hAdd = HAdd.hAdd) (h_mul : HMul.hMul = HMul.hMul) :

inst₁ = inst₂

theorem NonUnitalNonAssocSemiring.ext_iff {R : Type u} {inst₁ inst₂ : NonUnitalNonAssocSemiring R} :

inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul

theorem NonUnitalNonAssocSemiring.toDistrib_injective {R : Type u} :

Function.Injective (@toDistrib R)

NonUnitalSemiring #

theorem NonUnitalSemiring.toNonUnitalNonAssocSemiring_injective {R : Type u} :

Function.Injective (@toNonUnitalNonAssocSemiring R)

theorem NonUnitalSemiring.ext {R : Type u} ⦃inst₁ inst₂ : NonUnitalSemiring R⦄ (h_add : HAdd.hAdd = HAdd.hAdd) (h_mul : HMul.hMul = HMul.hMul) :

inst₁ = inst₂

theorem NonUnitalSemiring.ext_iff {R : Type u} {inst₁ inst₂ : NonUnitalSemiring R} :

inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul

NonAssocSemiring and its ancestors #

This section also includes results for AddMonoidWithOne, AddCommMonoidWithOne, etc. as these are considered implementation detail of the ring classes. TODO consider relocating these lemmas.

theorem AddMonoidWithOne.ext {R : Type u} ⦃inst₁ inst₂ : AddMonoidWithOne R⦄ (h_add : HAdd.hAdd = HAdd.hAdd) (h_one : One.one = One.one) :

inst₁ = inst₂

theorem AddMonoidWithOne.ext_iff {R : Type u} {inst₁ inst₂ : AddMonoidWithOne R} :

inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ One.one = One.one

theorem AddCommMonoidWithOne.toAddMonoidWithOne_injective {R : Type u} :

Function.Injective (@toAddMonoidWithOne R)

theorem AddCommMonoidWithOne.ext {R : Type u} ⦃inst₁ inst₂ : AddCommMonoidWithOne R⦄ (h_add : HAdd.hAdd = HAdd.hAdd) (h_one : One.one = One.one) :

inst₁ = inst₂

theorem AddCommMonoidWithOne.ext_iff {R : Type u} {inst₁ inst₂ : AddCommMonoidWithOne R} :

inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ One.one = One.one

theorem NonAssocSemiring.ext {R : Type u} ⦃inst₁ inst₂ : NonAssocSemiring R⦄ (h_add : HAdd.hAdd = HAdd.hAdd) (h_mul : HMul.hMul = HMul.hMul) :

inst₁ = inst₂

theorem NonAssocSemiring.ext_iff {R : Type u} {inst₁ inst₂ : NonAssocSemiring R} :

inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul

theorem NonAssocSemiring.toNonUnitalNonAssocSemiring_injective {R : Type u} :

Function.Injective (@toNonUnitalNonAssocSemiring R)

NonUnitalNonAssocRing #

theorem NonUnitalNonAssocRing.ext {R : Type u} ⦃inst₁ inst₂ : NonUnitalNonAssocRing R⦄ (h_add : HAdd.hAdd = HAdd.hAdd) (h_mul : HMul.hMul = HMul.hMul) :

inst₁ = inst₂

theorem NonUnitalNonAssocRing.ext_iff {R : Type u} {inst₁ inst₂ : NonUnitalNonAssocRing R} :

inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul

theorem NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring_injective {R : Type u} :

Function.Injective (@toNonUnitalNonAssocSemiring R)

NonUnitalRing #

theorem NonUnitalRing.ext {R : Type u} ⦃inst₁ inst₂ : NonUnitalRing R⦄ (h_add : HAdd.hAdd = HAdd.hAdd) (h_mul : HMul.hMul = HMul.hMul) :

inst₁ = inst₂

theorem NonUnitalRing.ext_iff {R : Type u} {inst₁ inst₂ : NonUnitalRing R} :

inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul

theorem NonUnitalRing.toNonUnitalSemiring_injective {R : Type u} :

Function.Injective (@toNonUnitalSemiring R)

theorem NonUnitalRing.toNonUnitalNonAssocring_injective {R : Type u} :

Function.Injective (@toNonUnitalNonAssocRing R)

NonAssocRing and its ancestors #

This section also includes results for AddGroupWithOne, AddCommGroupWithOne, etc. as these are considered implementation detail of the ring classes. TODO consider relocating these lemmas.

theorem AddGroupWithOne.ext {R : Type u} ⦃inst₁ inst₂ : AddGroupWithOne R⦄ (h_add : HAdd.hAdd = HAdd.hAdd) (h_one : One.one = One.one) :

inst₁ = inst₂

theorem AddGroupWithOne.ext_iff {R : Type u} {inst₁ inst₂ : AddGroupWithOne R} :

inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ One.one = One.one

theorem AddCommGroupWithOne.ext {R : Type u} ⦃inst₁ inst₂ : AddCommGroupWithOne R⦄ (h_add : HAdd.hAdd = HAdd.hAdd) (h_one : One.one = One.one) :

inst₁ = inst₂

theorem AddCommGroupWithOne.ext_iff {R : Type u} {inst₁ inst₂ : AddCommGroupWithOne R} :

inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ One.one = One.one

theorem NonAssocRing.ext {R : Type u} ⦃inst₁ inst₂ : NonAssocRing R⦄ (h_add : HAdd.hAdd = HAdd.hAdd) (h_mul : HMul.hMul = HMul.hMul) :

inst₁ = inst₂

theorem NonAssocRing.ext_iff {R : Type u} {inst₁ inst₂ : NonAssocRing R} :

inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul

theorem NonAssocRing.toNonAssocSemiring_injective {R : Type u} :

Function.Injective (@toNonAssocSemiring R)

theorem NonAssocRing.toNonUnitalNonAssocring_injective {R : Type u} :

Function.Injective (@toNonUnitalNonAssocRing R)

Semiring #

theorem Semiring.ext {R : Type u} ⦃inst₁ inst₂ : Semiring R⦄ (h_add : HAdd.hAdd = HAdd.hAdd) (h_mul : HMul.hMul = HMul.hMul) :

inst₁ = inst₂

theorem Semiring.ext_iff {R : Type u} {inst₁ inst₂ : Semiring R} :

inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul

theorem Semiring.toNonUnitalSemiring_injective {R : Type u} :

Function.Injective (@toNonUnitalSemiring R)

theorem Semiring.toNonAssocSemiring_injective {R : Type u} :

Function.Injective (@toNonAssocSemiring R)

Ring #

theorem Ring.ext {R : Type u} ⦃inst₁ inst₂ : Ring R⦄ (h_add : HAdd.hAdd = HAdd.hAdd) (h_mul : HMul.hMul = HMul.hMul) :

inst₁ = inst₂

theorem Ring.ext_iff {R : Type u} {inst₁ inst₂ : Ring R} :

inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul

theorem Ring.toNonUnitalRing_injective {R : Type u} :

Function.Injective (@toNonUnitalRing R)

theorem Ring.toNonAssocRing_injective {R : Type u} :

Function.Injective (@toNonAssocRing R)

theorem Ring.toSemiring_injective {R : Type u} :

Function.Injective (@toSemiring R)

NonUnitalNonAssocCommSemiring #

theorem NonUnitalNonAssocCommSemiring.toNonUnitalNonAssocSemiring_injective {R : Type u} :

Function.Injective (@toNonUnitalNonAssocSemiring R)

theorem NonUnitalNonAssocCommSemiring.ext {R : Type u} ⦃inst₁ inst₂ : NonUnitalNonAssocCommSemiring R⦄ (h_add : HAdd.hAdd = HAdd.hAdd) (h_mul : HMul.hMul = HMul.hMul) :

inst₁ = inst₂

theorem NonUnitalNonAssocCommSemiring.ext_iff {R : Type u} {inst₁ inst₂ : NonUnitalNonAssocCommSemiring R} :

inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul

NonUnitalCommSemiring #

theorem NonUnitalCommSemiring.toNonUnitalSemiring_injective {R : Type u} :

Function.Injective (@toNonUnitalSemiring R)

theorem NonUnitalCommSemiring.ext {R : Type u} ⦃inst₁ inst₂ : NonUnitalCommSemiring R⦄ (h_add : HAdd.hAdd = HAdd.hAdd) (h_mul : HMul.hMul = HMul.hMul) :

inst₁ = inst₂

theorem NonUnitalCommSemiring.ext_iff {R : Type u} {inst₁ inst₂ : NonUnitalCommSemiring R} :

inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul

NonUnitalNonAssocCommRing #

theorem NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing_injective {R : Type u} :

Function.Injective (@toNonUnitalNonAssocRing R)

theorem NonUnitalNonAssocCommRing.ext {R : Type u} ⦃inst₁ inst₂ : NonUnitalNonAssocCommRing R⦄ (h_add : HAdd.hAdd = HAdd.hAdd) (h_mul : HMul.hMul = HMul.hMul) :

inst₁ = inst₂

theorem NonUnitalNonAssocCommRing.ext_iff {R : Type u} {inst₁ inst₂ : NonUnitalNonAssocCommRing R} :

inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul

NonUnitalCommRing #

theorem NonUnitalCommRing.toNonUnitalRing_injective {R : Type u} :

Function.Injective (@toNonUnitalRing R)

theorem NonUnitalCommRing.ext {R : Type u} ⦃inst₁ inst₂ : NonUnitalCommRing R⦄ (h_add : HAdd.hAdd = HAdd.hAdd) (h_mul : HMul.hMul = HMul.hMul) :

inst₁ = inst₂

theorem NonUnitalCommRing.ext_iff {R : Type u} {inst₁ inst₂ : NonUnitalCommRing R} :

inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul

CommSemiring #

theorem CommSemiring.toSemiring_injective {R : Type u} :

Function.Injective (@toSemiring R)

theorem CommSemiring.ext {R : Type u} ⦃inst₁ inst₂ : CommSemiring R⦄ (h_add : HAdd.hAdd = HAdd.hAdd) (h_mul : HMul.hMul = HMul.hMul) :

inst₁ = inst₂

theorem CommSemiring.ext_iff {R : Type u} {inst₁ inst₂ : CommSemiring R} :

inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul

CommRing #

theorem CommRing.toRing_injective {R : Type u} :

Function.Injective (@toRing R)

theorem CommRing.ext {R : Type u} ⦃inst₁ inst₂ : CommRing R⦄ (h_add : HAdd.hAdd = HAdd.hAdd) (h_mul : HMul.hMul = HMul.hMul) :

inst₁ = inst₂

theorem CommRing.ext_iff {R : Type u} {inst₁ inst₂ : CommRing R} :

inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul