English
For any RingCon c, the operation of transforming matrices via matrix mapping captures the original RingCon: ofMatrix (matrix n c) = c.
Русский
Для RingCon c операция преобразования матриц через матричное отображение возвращает исходный RingCon: ofMatrix (matrix n c) = c.
LaTeX
$$ofMatrix_matrix : ofMatrix (matrix n c) = c$$
Lean4
/-- The congruence relation induced by `c` on `single i j`. -/
def ofMatrix [DecidableEq n] (c : RingCon (Matrix n n R)) : RingCon R
where
r x y := ∀ i j, c (single i j x) (single i j y)
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 _ _ ↦ by simpa [single_add] using c.add (h₁ _ _) (h₂ _ _)
mul' h₁ h₂ := fun i j ↦ by simpa using c.mul (h₁ i i) (h₂ i j)
