# Congruence relations #

This file proves basic properties of the quotient of a type by a congruence relation.

The second half of the file concerns congruence relations on monoids, in which case the quotient by the congruence relation is also a monoid. There are results about the universal property of quotients of monoids, and the isomorphism theorems for monoids.

## Implementation notes #

A congruence relation on a monoid `M` can be thought of as a submonoid of `M × M` for which membership is an equivalence relation, but whilst this fact is established in the file, it is not used, since this perspective adds more layers of definitional unfolding.

## Tags #

congruence, congruence relation, quotient, quotient by congruence relation, monoid, quotient monoid, isomorphism theorems

source
def Con.prod {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (c : Con M) (d : Con N) :
Con (M × N)

Given types with multiplications `M, N`, the product of two congruence relations `c` on `M` and `d` on `N`: `(x₁, x₂), (y₁, y₂) ∈ M × N` are related by `c.prod d` iff `x₁` is related to `y₁` by `c` and `x₂` is related to `y₂` by `d`.

Equations

- c.prod d = { toSetoid := c.prod d.toSetoid, mul' := ⋯ }

Instances For

source
def AddCon.prod {M : Type u_1} {N : Type u_2} [Add M] [Add N] (c : AddCon M) (d : AddCon N) :
AddCon (M × N)

Given types with additions `M, N`, the product of two congruence relations `c` on `M` and `d` on `N`: `(x₁, x₂), (y₁, y₂) ∈ M × N` are related by `c.prod d` iff `x₁` is related to `y₁` by `c` and `x₂` is related to `y₂` by `d`.

Equations

- c.prod d = { toSetoid := c.prod d.toSetoid, add' := ⋯ }

Instances For

source
def Con.pi {ι : Type u_4} {f : ι → Type u_5} [(i : ι) → Mul (f i)] (C : (i : ι) → Con (f i)) :
Con ((i : ι) → f i)

The product of an indexed collection of congruence relations.

Equations

- Con.pi C = { toSetoid := piSetoid, mul' := ⋯ }

Instances For

source
def AddCon.pi {ι : Type u_4} {f : ι → Type u_5} [(i : ι) → Add (f i)] (C : (i : ι) → AddCon (f i)) :
AddCon ((i : ι) → f i)

The product of an indexed collection of additive congruence relations.

Equations

- AddCon.pi C = { toSetoid := piSetoid, add' := ⋯ }

Instances For

source
def Con.congr {M : Type u_1} [Mul M] {c d : Con M} (h : c = d) :
c.Quotient ≃* d.Quotient

Makes an isomorphism of quotients by two congruence relations, given that the relations are equal.

Equations

- Con.congr h = { toEquiv := Quotient.congr (Equiv.refl M) ⋯, map_mul' := ⋯ }

Instances For

source
def AddCon.congr {M : Type u_1} [Add M] {c d : AddCon M} (h : c = d) :
c.Quotient ≃+ d.Quotient

Makes an additive isomorphism of quotients by two additive congruence relations, given that the relations are equal.

Equations

- AddCon.congr h = { toEquiv := Quotient.congr (Equiv.refl M) ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem Con.congr_mk {M : Type u_1} [Mul M] {c d : Con M} (h : c = d) (a : M) :
(Con.congr h) ↑a = ↑a
source
@[simp]
theorem AddCon.congr_mk {M : Type u_1} [Add M] {c d : AddCon M} (h : c = d) (a : M) :
(AddCon.congr h) ↑a = ↑a
source
theorem Con.le_comap_conGen {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M → N) (H : ∀ (x y : M), f (x * y) = f x * f y) (rel : N → N → Prop) :
(conGen fun (x y : M) => rel (f x) (f y)) ≤ comap f H (conGen rel)
source
theorem AddCon.le_comap_conGen {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M → N) (H : ∀ (x y : M), f (x + y) = f x + f y) (rel : N → N → Prop) :
(addConGen fun (x y : M) => rel (f x) (f y)) ≤ comap f H (addConGen rel)
source
theorem Con.comap_conGen_equiv {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) (rel : N → N → Prop) :
comap ⇑f ⋯ (conGen rel) = conGen fun (x y : M) => rel (f x) (f y)
source
theorem AddCon.comap_conGen_equiv {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) (rel : N → N → Prop) :
comap ⇑f ⋯ (addConGen rel) = addConGen fun (x y : M) => rel (f x) (f y)
source
theorem Con.comap_conGen_of_bijective {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M → N) (hf : Function.Bijective f) (H : ∀ (x y : M), f (x * y) = f x * f y) (rel : N → N → Prop) :
comap f H (conGen rel) = conGen fun (x y : M) => rel (f x) (f y)
source
theorem AddCon.comap_conGen_of_bijective {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M → N) (hf : Function.Bijective f) (H : ∀ (x y : M), f (x + y) = f x + f y) (rel : N → N → Prop) :
comap f H (addConGen rel) = addConGen fun (x y : M) => rel (f x) (f y)
source
def Con.submonoid {M : Type u_1} [MulOneClass M] (c : Con M) :
Submonoid (M × M)

The submonoid of `M × M` defined by a congruence relation on a monoid `M`.

Equations

- ↑c = { carrier := {x : M × M | c x.1 x.2}, mul_mem' := ⋯, one_mem' := ⋯ }

Instances For

source
def AddCon.addSubmonoid {M : Type u_1} [AddZeroClass M] (c : AddCon M) :
AddSubmonoid (M × M)

The `AddSubmonoid` of `M × M` defined by an additive congruence relation on an `AddMonoid` `M`.

Equations

- ↑c = { carrier := {x : M × M | c x.1 x.2}, add_mem' := ⋯, zero_mem' := ⋯ }

Instances For

source
def Con.ofSubmonoid {M : Type u_1} [MulOneClass M] (N : Submonoid (M × M)) (H : Equivalence fun (x y : M) => (x, y) ∈ N) :
Con M

The congruence relation on a monoid `M` from a submonoid of `M × M` for which membership is an equivalence relation.

Equations

- Con.ofSubmonoid N H = { r := fun (x y : M) => (x, y) ∈ N, iseqv := H, mul' := ⋯ }

Instances For

source
def AddCon.ofAddSubmonoid {M : Type u_1} [AddZeroClass M] (N : AddSubmonoid (M × M)) (H : Equivalence fun (x y : M) => (x, y) ∈ N) :
AddCon M

The additive congruence relation on an `AddMonoid` `M` from an `AddSubmonoid` of `M × M` for which membership is an equivalence relation.

Equations

- AddCon.ofAddSubmonoid N H = { r := fun (x y : M) => (x, y) ∈ N, iseqv := H, add' := ⋯ }

Instances For

source
instance Con.toSubmonoid {M : Type u_1} [MulOneClass M] :
Coe (Con M) (Submonoid (M × M))

Coercion from a congruence relation `c` on a monoid `M` to the submonoid of `M × M` whose elements are `(x, y)` such that `x` is related to `y` by `c`.

Equations

- Con.toSubmonoid = { coe := fun (c : Con M) => ↑c }

source
instance AddCon.toAddSubmonoid {M : Type u_1} [AddZeroClass M] :
Coe (AddCon M) (AddSubmonoid (M × M))

Coercion from a congruence relation `c` on an `AddMonoid` `M` to the `AddSubmonoid` of `M × M` whose elements are `(x, y)` such that `x` is related to `y` by `c`.

Equations

- AddCon.toAddSubmonoid = { coe := fun (c : AddCon M) => ↑c }

source
theorem Con.mem_coe {M : Type u_1} [MulOneClass M] {c : Con M} {x y : M} :
(x, y) ∈ ↑c ↔ (x, y) ∈ c
source
theorem AddCon.mem_coe {M : Type u_1} [AddZeroClass M] {c : AddCon M} {x y : M} :
(x, y) ∈ ↑c ↔ (x, y) ∈ c
source
theorem Con.to_submonoid_inj {M : Type u_1} [MulOneClass M] (c d : Con M) (H : ↑c = ↑d) :
c = d
source
theorem AddCon.to_addSubmonoid_inj {M : Type u_1} [AddZeroClass M] (c d : AddCon M) (H : ↑c = ↑d) :
c = d
source
theorem Con.le_iff {M : Type u_1} [MulOneClass M] {c d : Con M} :
c ≤ d ↔ ↑c ≤ ↑d
source
theorem AddCon.le_iff {M : Type u_1} [AddZeroClass M] {c d : AddCon M} :
c ≤ d ↔ ↑c ≤ ↑d
source
@[simp]
theorem Con.mrange_mk' {M : Type u_1} [MulOneClass M] {c : Con M} :
MonoidHom.mrange c.mk' = ⊤
source
@[simp]
theorem AddCon.mrange_mk' {M : Type u_1} [AddZeroClass M] {c : AddCon M} :
AddMonoidHom.mrange c.mk' = ⊤
source
theorem Con.lift_range {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {c : Con M} {f : M →* P} (H : c ≤ ker f) :
MonoidHom.mrange (c.lift f H) = MonoidHom.mrange f

Given a congruence relation `c` on a monoid and a homomorphism `f` constant on `c`'s equivalence classes, `f` has the same image as the homomorphism that `f` induces on the quotient.

source
theorem AddCon.lift_range {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] {c : AddCon M} {f : M →+ P} (H : c ≤ ker f) :
AddMonoidHom.mrange (c.lift f H) = AddMonoidHom.mrange f

Given an additive congruence relation `c` on an `AddMonoid` and a homomorphism `f` constant on `c`'s equivalence classes, `f` has the same image as the homomorphism that `f` induces on the quotient.

source
@[simp]
theorem Con.kerLift_range_eq {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {f : M →* P} :
MonoidHom.mrange (kerLift f) = MonoidHom.mrange f

Given a monoid homomorphism `f`, the induced homomorphism on the quotient by `f`'s kernel has the same image as `f`.

source
@[simp]
theorem AddCon.kerLift_range_eq {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] {f : M →+ P} :
AddMonoidHom.mrange (kerLift f) = AddMonoidHom.mrange f

Given an `AddMonoid` homomorphism `f`, the induced homomorphism on the quotient by `f`'s kernel has the same image as `f`.

source
noncomputable def Con.quotientKerEquivRange {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] (f : M →* P) :
(ker f).Quotient ≃* ↥(MonoidHom.mrange f)

The first isomorphism theorem for monoids.

Equations

- Con.quotientKerEquivRange f = { toEquiv := Equiv.ofBijective ⇑((MulEquiv.submonoidCongr ⋯).toMonoidHom.comp (Con.kerLift f).mrangeRestrict) ⋯, map_mul' := ⋯ }

Instances For

source
noncomputable def AddCon.quotientKerEquivRange {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] (f : M →+ P) :
(ker f).Quotient ≃+ ↥(AddMonoidHom.mrange f)

The first isomorphism theorem for `AddMonoid`s.

Equations

- AddCon.quotientKerEquivRange f = { toEquiv := Equiv.ofBijective ⇑((AddEquiv.addSubmonoidCongr ⋯).toAddMonoidHom.comp (AddCon.kerLift f).mrangeRestrict) ⋯, map_add' := ⋯ }

Instances For

source
def Con.quotientKerEquivOfRightInverse {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] (f : M →* P) (g : P → M) (hf : Function.RightInverse g ⇑f) :
(ker f).Quotient ≃* P

The first isomorphism theorem for monoids in the case of a homomorphism with right inverse.

Equations

- Con.quotientKerEquivOfRightInverse f g hf = { toFun := ⇑(Con.kerLift f), invFun := Con.toQuotient ∘ g, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

Instances For

source
def AddCon.quotientKerEquivOfRightInverse {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] (f : M →+ P) (g : P → M) (hf : Function.RightInverse g ⇑f) :
(ker f).Quotient ≃+ P

The first isomorphism theorem for `AddMonoid`s in the case of a homomorphism with right inverse.

Equations

- AddCon.quotientKerEquivOfRightInverse f g hf = { toFun := ⇑(AddCon.kerLift f), invFun := AddCon.toQuotient ∘ g, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem Con.quotientKerEquivOfRightInverse_apply {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] (f : M →* P) (g : P → M) (hf : Function.RightInverse g ⇑f) (a : (ker f).Quotient) :
(quotientKerEquivOfRightInverse f g hf) a = (kerLift f) a
source
@[simp]
theorem Con.quotientKerEquivOfRightInverse_symm_apply {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] (f : M →* P) (g : P → M) (hf : Function.RightInverse g ⇑f) (a✝ : P) :
(quotientKerEquivOfRightInverse f g hf).symm a✝ = (toQuotient ∘ g) a✝
source
@[simp]
theorem AddCon.quotientKerEquivOfRightInverse_apply {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] (f : M →+ P) (g : P → M) (hf : Function.RightInverse g ⇑f) (a : (ker f).Quotient) :
(quotientKerEquivOfRightInverse f g hf) a = (kerLift f) a
source
@[simp]
theorem AddCon.quotientKerEquivOfRightInverse_symm_apply {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] (f : M →+ P) (g : P → M) (hf : Function.RightInverse g ⇑f) (a✝ : P) :
(quotientKerEquivOfRightInverse f g hf).symm a✝ = (toQuotient ∘ g) a✝
source
noncomputable def Con.quotientKerEquivOfSurjective {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] (f : M →* P) (hf : Function.Surjective ⇑f) :
(ker f).Quotient ≃* P

The first isomorphism theorem for Monoids in the case of a surjective homomorphism.

For a `computable` version, see `Con.quotientKerEquivOfRightInverse`.

Equations

- Con.quotientKerEquivOfSurjective f hf = Con.quotientKerEquivOfRightInverse f (Exists.choose ⋯) ⋯

Instances For

source
noncomputable def AddCon.quotientKerEquivOfSurjective {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] (f : M →+ P) (hf : Function.Surjective ⇑f) :
(ker f).Quotient ≃+ P

The first isomorphism theorem for `AddMonoid`s in the case of a surjective homomorphism.

For a `computable` version, see `AddCon.quotientKerEquivOfRightInverse`.

Equations

- AddCon.quotientKerEquivOfSurjective f hf = AddCon.quotientKerEquivOfRightInverse f (Exists.choose ⋯) ⋯

Instances For

source
noncomputable def Con.comapQuotientEquivOfSurj {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (c : Con M) (f : N →* M) (hf : Function.Surjective ⇑f) :
(comap ⇑f ⋯ c).Quotient ≃* c.Quotient

If e : M →* N is surjective then (c.comap e).Quotient ≃* c.Quotient with c : Con N

Equations

- c.comapQuotientEquivOfSurj f hf = (Con.congr ⋯).trans (Con.quotientKerEquivOfSurjective (c.mk'.comp f) ⋯)

Instances For

source
noncomputable def AddCon.comapQuotientEquivOfSurj {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (c : AddCon M) (f : N →+ M) (hf : Function.Surjective ⇑f) :
(comap ⇑f ⋯ c).Quotient ≃+ c.Quotient

If e : M →* N is surjective then (c.comap e).Quotient ≃* c.Quotient with c : AddCon N

Equations

- c.comapQuotientEquivOfSurj f hf = (AddCon.congr ⋯).trans (AddCon.quotientKerEquivOfSurjective (c.mk'.comp f) ⋯)

Instances For

source
@[simp]
theorem Con.comapQuotientEquivOfSurj_mk {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (c : Con M) {f : N →* M} (hf : Function.Surjective ⇑f) (x : N) :
(c.comapQuotientEquivOfSurj f hf) ↑x = ↑(f x)
source
@[simp]
theorem AddCon.comapQuotientEquivOfSurj_mk {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (c : AddCon M) {f : N →+ M} (hf : Function.Surjective ⇑f) (x : N) :
(c.comapQuotientEquivOfSurj f hf) ↑x = ↑(f x)
source
@[simp]
theorem Con.comapQuotientEquivOfSurj_symm_mk {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (c : Con M) {f : N →* M} (hf : Function.Surjective ⇑f) (x : N) :
(c.comapQuotientEquivOfSurj f hf).symm ↑(f x) = ↑x
source
@[simp]
theorem AddCon.comapQuotientEquivOfSurj_symm_mk {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (c : AddCon M) {f : N →+ M} (hf : Function.Surjective ⇑f) (x : N) :
(c.comapQuotientEquivOfSurj f hf).symm ↑(f x) = ↑x
source
@[simp]
theorem Con.comapQuotientEquivOfSurj_symm_mk' {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (c : Con M) (f : N ≃* M) (x : N) :
(c.comapQuotientEquivOfSurj ↑f ⋯).symm ⟦f x⟧ = ↑x

This version infers the surjectivity of the function from a MulEquiv function

source
@[simp]
theorem AddCon.comapQuotientEquivOfSurj_symm_mk' {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (c : AddCon M) (f : N ≃+ M) (x : N) :
(c.comapQuotientEquivOfSurj ↑f ⋯).symm ⟦f x⟧ = ↑x

This version infers the surjectivity of the function from a MulEquiv function

source
noncomputable def Con.comapQuotientEquiv {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (c : Con M) (f : N →* M) :
(comap ⇑f ⋯ c).Quotient ≃* ↥(MonoidHom.mrange (c.mk'.comp f))

The second isomorphism theorem for monoids.

Equations

- c.comapQuotientEquiv f = (Con.congr ⋯).trans (Con.quotientKerEquivRange (c.mk'.comp f))

Instances For

source
noncomputable def AddCon.comapQuotientEquiv {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (c : AddCon M) (f : N →+ M) :
(comap ⇑f ⋯ c).Quotient ≃+ ↥(AddMonoidHom.mrange (c.mk'.comp f))

The second isomorphism theorem for `AddMonoid`s.

Equations

- c.comapQuotientEquiv f = (AddCon.congr ⋯).trans (AddCon.quotientKerEquivRange (c.mk'.comp f))

Instances For

source
def Con.quotientQuotientEquivQuotient {M : Type u_1} [MulOneClass M] (c d : Con M) (h : c ≤ d) :
(ker (c.map d h)).Quotient ≃* d.Quotient

The third isomorphism theorem for monoids.

Equations

- c.quotientQuotientEquivQuotient d h = { toEquiv := c.quotientQuotientEquivQuotient d.toSetoid h, map_mul' := ⋯ }

Instances For

source
def AddCon.quotientQuotientEquivQuotient {M : Type u_1} [AddZeroClass M] (c d : AddCon M) (h : c ≤ d) :
(ker (c.map d h)).Quotient ≃+ d.Quotient

The third isomorphism theorem for `AddMonoid`s.

Equations

- c.quotientQuotientEquivQuotient d h = { toEquiv := c.quotientQuotientEquivQuotient d.toSetoid h, map_add' := ⋯ }

Instances For

source
theorem Con.smul {α : Type u_4} {M : Type u_5} [MulOneClass M] [SMul α M] [IsScalarTower α M M] (c : Con M) (a : α) {w x : M} (h : c w x) :
c (a • w) (a • x)
source
theorem AddCon.vadd {α : Type u_4} {M : Type u_5} [AddZeroClass M] [VAdd α M] [VAddAssocClass α M M] (c : AddCon M) (a : α) {w x : M} (h : c w x) :
c (a +ᵥ w) (a +ᵥ x)
source
instance Con.instSMul {α : Type u_4} {M : Type u_5} [MulOneClass M] [SMul α M] [IsScalarTower α M M] (c : Con M) :
SMul α c.Quotient
Equations

- c.instSMul = { smul := fun (a : α) => Quotient.map' (fun (x : M) => a • x) ⋯ }

source
instance AddCon.instVAdd {α : Type u_4} {M : Type u_5} [AddZeroClass M] [VAdd α M] [VAddAssocClass α M M] (c : AddCon M) :
VAdd α c.Quotient
Equations

- c.instVAdd = { vadd := fun (a : α) => Quotient.map' (fun (x : M) => a +ᵥ x) ⋯ }

source
theorem Con.coe_smul {α : Type u_4} {M : Type u_5} [MulOneClass M] [SMul α M] [IsScalarTower α M M] (c : Con M) (a : α) (x : M) :
↑(a • x) = a • ↑x
source
theorem AddCon.coe_vadd {α : Type u_4} {M : Type u_5} [AddZeroClass M] [VAdd α M] [VAddAssocClass α M M] (c : AddCon M) (a : α) (x : M) :
↑(a +ᵥ x) = a +ᵥ ↑x
source
instance Con.instSMulCommClass {α : Type u_4} {β : Type u_5} {M : Type u_6} [MulOneClass M] [SMul α M] [SMul β M] [IsScalarTower α M M] [IsScalarTower β M M] [SMulCommClass α β M] (c : Con M) :
SMulCommClass α β c.Quotient
source
instance Con.instIsScalarTower {α : Type u_4} {β : Type u_5} {M : Type u_6} [MulOneClass M] [SMul α β] [SMul α M] [SMul β M] [IsScalarTower α M M] [IsScalarTower β M M] [IsScalarTower α β M] (c : Con M) :
IsScalarTower α β c.Quotient
source
instance Con.instIsCentralScalar {α : Type u_4} {M : Type u_5} [MulOneClass M] [SMul α M] [SMul α ᵐᵒᵖ M] [IsScalarTower α M M] [IsScalarTower α ᵐᵒᵖ M M] [IsCentralScalar α M] (c : Con M) :
IsCentralScalar α c.Quotient
source
instance Con.mulAction {α : Type u_4} {M : Type u_5} [Monoid α] [MulOneClass M] [MulAction α M] [IsScalarTower α M M] (c : Con M) :
MulAction α c.Quotient
Equations

- c.mulAction = { toSMul := c.instSMul, one_smul := ⋯, mul_smul := ⋯ }

source
instance AddCon.addAction {α : Type u_4} {M : Type u_5} [AddMonoid α] [AddZeroClass M] [AddAction α M] [VAddAssocClass α M M] (c : AddCon M) :
AddAction α c.Quotient
Equations

- c.addAction = { toVAdd := c.instVAdd, zero_vadd := ⋯, add_vadd := ⋯ }

source
instance Con.mulDistribMulAction {α : Type u_4} {M : Type u_5} [Monoid α] [Monoid M] [MulDistribMulAction α M] [IsScalarTower α M M] (c : Con M) :
MulDistribMulAction α c.Quotient
Equations

- c.mulDistribMulAction = { toMulAction := c.mulAction, smul_mul := ⋯, smul_one := ⋯ }