English
The matrix congruence associated to a RingCon c acts entrywise on matrices: c.matrix n M N iff ∀ i j, c (M_{ij}) (N_{ij}).
Русский
Связь конгруэнции RingCon действует по каждому элементу матрицы: c.matrix n M N тогда и только тогда, когда ∀ i j, c(M_{ij}) (N_{ij}).
LaTeX
$$c.matrix n M N ⇔ ∀ i j, c (M_{i j}) (N_{i j})$$
Lean4
/-- The ring congruence of matrices with entries related by `c`. -/
def matrix (c : RingCon R) : RingCon (Matrix n n R)
where
r M
N :=
∀ i j,
c (M i j)
(N i j)
-- note: kept `fun` to distinguish `RingCon`'s binders from `r`'s binders.
iseqv.refl _ := fun _ _ ↦ c.refl _
iseqv.symm h := fun _ _ ↦ c.symm <| h _ _
iseqv.trans h₁ h₂ := fun _ _ ↦ c.trans (h₁ _ _) (h₂ _ _)
add' h₁ h₂ := fun _ _ ↦ c.add (h₁ _ _) (h₂ _ _)
mul' h₁ h₂ := fun _ _ ↦ c.finset_sum _ fun _ _ => c.mul (h₁ _ _) (h₂ _ _)
