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_iff {R : Type u} {inst₁ : Distrib R} {inst₂ : Distrib R} :
inst₁ = inst₂ HAdd.hAdd = HAdd.hAdd HMul.hMul = HMul.hMul
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₂

NonUnitalNonAssocSemiring #

theorem NonUnitalNonAssocSemiring.ext_iff {R : Type u} {inst₁ : NonUnitalNonAssocSemiring R} {inst₂ : NonUnitalNonAssocSemiring R} :
inst₁ = inst₂ HAdd.hAdd = HAdd.hAdd HMul.hMul = HMul.hMul
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₂

NonUnitalSemiring #

theorem NonUnitalSemiring.ext_iff {R : Type u} {inst₁ : NonUnitalSemiring R} {inst₂ : NonUnitalSemiring R} :
inst₁ = inst₂ HAdd.hAdd = HAdd.hAdd HMul.hMul = HMul.hMul
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₂

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_iff {R : Type u} {inst₁ : AddMonoidWithOne R} {inst₂ : AddMonoidWithOne R} :
inst₁ = inst₂ HAdd.hAdd = HAdd.hAdd One.one = One.one
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.ext_iff {R : Type u} {inst₁ : AddCommMonoidWithOne R} {inst₂ : AddCommMonoidWithOne R} :
inst₁ = inst₂ HAdd.hAdd = HAdd.hAdd One.one = One.one
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_iff {R : Type u} {inst₁ : NonAssocSemiring R} {inst₂ : NonAssocSemiring R} :
inst₁ = inst₂ HAdd.hAdd = HAdd.hAdd HMul.hMul = HMul.hMul
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₂

NonUnitalNonAssocRing #

theorem NonUnitalNonAssocRing.ext_iff {R : Type u} {inst₁ : NonUnitalNonAssocRing R} {inst₂ : NonUnitalNonAssocRing R} :
inst₁ = inst₂ HAdd.hAdd = HAdd.hAdd HMul.hMul = HMul.hMul
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₂

NonUnitalRing #

theorem NonUnitalRing.ext_iff {R : Type u} {inst₁ : NonUnitalRing R} {inst₂ : NonUnitalRing R} :
inst₁ = inst₂ HAdd.hAdd = HAdd.hAdd HMul.hMul = HMul.hMul
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₂

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_iff {R : Type u} {inst₁ : AddGroupWithOne R} {inst₂ : AddGroupWithOne R} :
inst₁ = inst₂ HAdd.hAdd = HAdd.hAdd One.one = One.one
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_iff {R : Type u} {inst₁ : AddCommGroupWithOne R} {inst₂ : AddCommGroupWithOne R} :
inst₁ = inst₂ HAdd.hAdd = HAdd.hAdd One.one = One.one
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_iff {R : Type u} {inst₁ : NonAssocRing R} {inst₂ : NonAssocRing R} :
inst₁ = inst₂ HAdd.hAdd = HAdd.hAdd HMul.hMul = HMul.hMul
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₂

Semiring #

theorem Semiring.ext_iff {R : Type u} {inst₁ : Semiring R} {inst₂ : Semiring R} :
inst₁ = inst₂ HAdd.hAdd = HAdd.hAdd HMul.hMul = HMul.hMul
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₂

Ring #

theorem Ring.ext_iff {R : Type u} {inst₁ : Ring R} {inst₂ : Ring R} :
inst₁ = inst₂ HAdd.hAdd = HAdd.hAdd HMul.hMul = HMul.hMul
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₂

NonUnitalNonAssocCommSemiring #

theorem NonUnitalNonAssocCommSemiring.ext_iff {R : Type u} {inst₁ : NonUnitalNonAssocCommSemiring R} {inst₂ : NonUnitalNonAssocCommSemiring R} :
inst₁ = inst₂ HAdd.hAdd = HAdd.hAdd HMul.hMul = HMul.hMul
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₂

NonUnitalCommSemiring #

theorem NonUnitalCommSemiring.ext_iff {R : Type u} {inst₁ : NonUnitalCommSemiring R} {inst₂ : NonUnitalCommSemiring R} :
inst₁ = inst₂ HAdd.hAdd = HAdd.hAdd HMul.hMul = HMul.hMul
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₂

NonUnitalNonAssocCommRing #

theorem NonUnitalNonAssocCommRing.ext_iff {R : Type u} {inst₁ : NonUnitalNonAssocCommRing R} {inst₂ : NonUnitalNonAssocCommRing R} :
inst₁ = inst₂ HAdd.hAdd = HAdd.hAdd HMul.hMul = HMul.hMul
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₂

NonUnitalCommRing #

theorem NonUnitalCommRing.ext_iff {R : Type u} {inst₁ : NonUnitalCommRing R} {inst₂ : NonUnitalCommRing R} :
inst₁ = inst₂ HAdd.hAdd = HAdd.hAdd HMul.hMul = HMul.hMul
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₂

CommSemiring #

theorem CommSemiring.ext_iff {R : Type u} {inst₁ : CommSemiring R} {inst₂ : CommSemiring R} :
inst₁ = inst₂ HAdd.hAdd = HAdd.hAdd HMul.hMul = HMul.hMul
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₂

CommRing #

theorem CommRing.ext_iff {R : Type u} {inst₁ : CommRing R} {inst₂ : CommRing R} :
inst₁ = inst₂ HAdd.hAdd = HAdd.hAdd HMul.hMul = HMul.hMul
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₂