Theorems · Definition · ring theory
RingCon.matrix
{R : Type u_1} →
(n : Type u_2) → [inst : NonUnitalNonAssocSemiring R] → [inst_1 : Fintype n] → RingCon R → RingCon (Matrix n n R)The ring congruence of matrices with entries related by c.
- Defined in
- Mathlib.LinearAlgebra.Matrix.Ideal
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Fintypestatement and proof · cited by 7,736
- Matrixstatement and proof · cited by 4,303
- NonUnitalNonAssocSemiringstatement and proof · cited by 1,081
- RingConstatement and proof · cited by 219
Cited by11
Results whose statement or proof uses this declaration.
- TwoSidedIdeal.matrixproof · cited by 10
- RingCon.matrix_injectivestatement and proof · cited by 2
- RingCon.matrix_apply_singlestatement and proof · cited by 1
- RingCon.matrix_botstatement and proof · cited by 1
- RingCon.matrix_monotonestatement and proof · cited by 1
- RingCon.matrix_topstatement · cited by 1
- RingCon.ofMatrix_matrixstatement and proof · cited by 0
- RingCon.matrix_applystatement · cited by 0
- RingCon.matrix_ofMatrixstatement and proof · cited by 0
- RingCon.matrix_strictMono_of_nonemptystatement · cited by 0
- TwoSidedIdeal.matrix_ringConstatement · cited by 0