English
The product of two congruence relations c on M and d on N is the congruence on M × N defined by (x1, x2) ~ (y1, y2) iff x1 ~c y1 and x2 ~d y2.
Русский
Произведение двух конгруэнций c на M и d на N задаёт конгруэнцию на M × N: (x1,x2) ~ (y1,y2) тогда и только если x1 ~c y1 и x2 ~d y2.
LaTeX
$$Con.prod c d is a congruence on M × N$$
Lean4
/-- 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`. -/
@[to_additive prod /-- 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`. -/
]
protected def prod (c : Con M) (d : Con N) : Con (M × N) :=
{ c.toSetoid.prod d.toSetoid with mul' := fun h1 h2 => ⟨c.mul h1.1 h2.1, d.mul h1.2 h2.2⟩ }
