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₁ : Distrib R⦄ ⦃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₁ : Distrib R} {inst₂ : Distrib R} :

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

NonUnitalNonAssocSemiring #

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

inst₁ = inst₂

theorem NonUnitalNonAssocSemiring.toDistrib_injective {R : Type u} :

Function.Injective (@NonUnitalNonAssocSemiring.toDistrib R)

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

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

NonUnitalSemiring #

theorem NonUnitalSemiring.toNonUnitalNonAssocSemiring_injective {R : Type u} :

Function.Injective (@NonUnitalSemiring.toNonUnitalNonAssocSemiring R)

theorem NonUnitalSemiring.ext {R : Type u} ⦃inst₁ : NonUnitalSemiring R⦄ ⦃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₁ : NonUnitalSemiring R} {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₁ : AddMonoidWithOne R⦄ ⦃inst₂ : AddMonoidWithOne R⦄ (h_add : HAdd.hAdd = HAdd.hAdd) (h_one : One.one = One.one) :

inst₁ = inst₂

theorem AddCommMonoidWithOne.toAddMonoidWithOne_injective {R : Type u} :

Function.Injective (@AddCommMonoidWithOne.toAddMonoidWithOne R)

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

inst₁ = inst₂

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

inst₁ = inst₂

theorem NonAssocSemiring.toNonUnitalNonAssocSemiring_injective {R : Type u} :

Function.Injective (@NonAssocSemiring.toNonUnitalNonAssocSemiring R)

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

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

NonUnitalNonAssocRing #

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

inst₁ = inst₂

theorem NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring_injective {R : Type u} :

Function.Injective (@NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring R)

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

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

NonUnitalRing #

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

inst₁ = inst₂

theorem NonUnitalRing.toNonUnitalSemiring_injective {R : Type u} :

Function.Injective (@NonUnitalRing.toNonUnitalSemiring R)

theorem NonUnitalRing.toNonUnitalNonAssocring_injective {R : Type u} :

Function.Injective (@NonUnitalRing.toNonUnitalNonAssocRing R)

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

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

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₁ : AddGroupWithOne R⦄ ⦃inst₂ : AddGroupWithOne R⦄ (h_add : HAdd.hAdd = HAdd.hAdd) (h_one : One.one = One.one) :

inst₁ = inst₂

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

inst₁ = inst₂

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

inst₁ = inst₂

theorem NonAssocRing.toNonAssocSemiring_injective {R : Type u} :

Function.Injective (@NonAssocRing.toNonAssocSemiring R)

theorem NonAssocRing.toNonUnitalNonAssocring_injective {R : Type u} :

Function.Injective (@NonAssocRing.toNonUnitalNonAssocRing R)

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

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

Semiring #

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

inst₁ = inst₂

theorem Semiring.toNonUnitalSemiring_injective {R : Type u} :

Function.Injective (@Semiring.toNonUnitalSemiring R)

theorem Semiring.toNonAssocSemiring_injective {R : Type u} :

Function.Injective (@Semiring.toNonAssocSemiring R)

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

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

Ring #

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

inst₁ = inst₂

theorem Ring.toNonUnitalRing_injective {R : Type u} :

Function.Injective (@Ring.toNonUnitalRing R)

theorem Ring.toNonAssocRing_injective {R : Type u} :

Function.Injective (@Ring.toNonAssocRing R)

theorem Ring.toSemiring_injective {R : Type u} :

Function.Injective (@Ring.toSemiring R)

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

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

NonUnitalNonAssocCommSemiring #

theorem NonUnitalNonAssocCommSemiring.toNonUnitalNonAssocSemiring_injective {R : Type u} :

Function.Injective (@NonUnitalNonAssocCommSemiring.toNonUnitalNonAssocSemiring R)

theorem NonUnitalNonAssocCommSemiring.ext {R : Type u} ⦃inst₁ : NonUnitalNonAssocCommSemiring R⦄ ⦃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₁ : NonUnitalNonAssocCommSemiring R} {inst₂ : NonUnitalNonAssocCommSemiring R} :

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

NonUnitalCommSemiring #

theorem NonUnitalCommSemiring.toNonUnitalSemiring_injective {R : Type u} :

Function.Injective (@NonUnitalCommSemiring.toNonUnitalSemiring R)

theorem NonUnitalCommSemiring.ext {R : Type u} ⦃inst₁ : NonUnitalCommSemiring R⦄ ⦃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₁ : NonUnitalCommSemiring R} {inst₂ : NonUnitalCommSemiring R} :

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

NonUnitalNonAssocCommRing #

theorem NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing_injective {R : Type u} :

Function.Injective (@NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing R)

theorem NonUnitalNonAssocCommRing.ext {R : Type u} ⦃inst₁ : NonUnitalNonAssocCommRing R⦄ ⦃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₁ : NonUnitalNonAssocCommRing R} {inst₂ : NonUnitalNonAssocCommRing R} :

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

NonUnitalCommRing #

theorem NonUnitalCommRing.toNonUnitalRing_injective {R : Type u} :

Function.Injective (@NonUnitalCommRing.toNonUnitalRing R)

theorem NonUnitalCommRing.ext {R : Type u} ⦃inst₁ : NonUnitalCommRing R⦄ ⦃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₁ : NonUnitalCommRing R} {inst₂ : NonUnitalCommRing R} :

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

CommSemiring #

theorem CommSemiring.toSemiring_injective {R : Type u} :

Function.Injective (@CommSemiring.toSemiring R)

theorem CommSemiring.ext {R : Type u} ⦃inst₁ : CommSemiring R⦄ ⦃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₁ : CommSemiring R} {inst₂ : CommSemiring R} :

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

CommRing #

theorem CommRing.toRing_injective {R : Type u} :

Function.Injective (@CommRing.toRing R)

theorem CommRing.ext {R : Type u} ⦃inst₁ : CommRing R⦄ ⦃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₁ : CommRing R} {inst₂ : CommRing R} :

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