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₂

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.toDistrib_injective {R : Type u} :

Function.Injective (@NonUnitalNonAssocSemiring.toDistrib R)

NonUnitalSemiring #

theorem NonUnitalSemiring.toNonUnitalNonAssocSemiring_injective {R : Type u} :

Function.Injective (@NonUnitalSemiring.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₂

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 AddCommMonoidWithOne.toAddMonoidWithOne_injective {R : Type u} :

Function.Injective (@AddCommMonoidWithOne.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 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.toNonUnitalNonAssocSemiring_injective {R : Type u} :

Function.Injective (@NonAssocSemiring.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.toNonUnitalNonAssocSemiring_injective {R : Type u} :

Function.Injective (@NonUnitalNonAssocRing.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.toNonUnitalSemiring_injective {R : Type u} :

Function.Injective (@NonUnitalRing.toNonUnitalSemiring R)

theorem NonUnitalRing.toNonUnitalNonAssocring_injective {R : Type u} :

Function.Injective (@NonUnitalRing.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 AddCommGroupWithOne.ext {R : Type u} ⦃inst₁ inst₂ : AddCommGroupWithOne R⦄ (h_add : HAdd.hAdd = HAdd.hAdd) (h_one : One.one = One.one) :

inst₁ = inst₂

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.toNonAssocSemiring_injective {R : Type u} :

Function.Injective (@NonAssocRing.toNonAssocSemiring R)

theorem NonAssocRing.toNonUnitalNonAssocring_injective {R : Type u} :

Function.Injective (@NonAssocRing.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.toNonUnitalSemiring_injective {R : Type u} :

Function.Injective (@Semiring.toNonUnitalSemiring R)

theorem Semiring.toNonAssocSemiring_injective {R : Type u} :

Function.Injective (@Semiring.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.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)

NonUnitalNonAssocCommSemiring #

theorem NonUnitalNonAssocCommSemiring.toNonUnitalNonAssocSemiring_injective {R : Type u} :

Function.Injective (@NonUnitalNonAssocCommSemiring.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₂

NonUnitalCommSemiring #

theorem NonUnitalCommSemiring.toNonUnitalSemiring_injective {R : Type u} :

Function.Injective (@NonUnitalCommSemiring.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₂

NonUnitalNonAssocCommRing #

theorem NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing_injective {R : Type u} :

Function.Injective (@NonUnitalNonAssocCommRing.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₂

NonUnitalCommRing #

theorem NonUnitalCommRing.toNonUnitalRing_injective {R : Type u} :

Function.Injective (@NonUnitalCommRing.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₂

CommSemiring #

theorem CommSemiring.toSemiring_injective {R : Type u} :

Function.Injective (@CommSemiring.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₂

CommRing #

theorem CommRing.toRing_injective {R : Type u} :

Function.Injective (@CommRing.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₂