Theorems · Theorem · ring theory

RingCon.matrix_ofMatrix

∀ {R : Type u_1} {n : Type u_2} [inst : NonAssocSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (c : RingCon (Matrix n n R)), RingCon.matrix n c.ofMatrix = c

Note that this does not apply to a non-unital ring, with counterexample where the elementwise congruence relation !![⊤,⊤;⊤,(· ≡ · [PMOD 4])] is a ring congruence over Matrix (Fin 2) (Fin 2) 2ℤ.

Defined in

Mathlib.LinearAlgebra.Matrix.Ideal

Cited by

0 results in Mathlib

Foundations

Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NonAssocSemiringFintypeDecidableEq