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

The best place to prove that the NatCast is determined by the other operations is probably in an extensionality lemma for AddMonoidWithOne, in which case we may as well do the typeclasses defined in Mathlib/Algebra/GroupWithZero/Defs.lean as well.

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