Theorems · Definition · linear algebra
Subsemiring.matrix
{n : Type u_3} →
{R : Type u_14} →
[inst : NonAssocSemiring R] →
[inst_1 : Fintype n] → [inst_2 : DecidableEq n] → Subsemiring R → Subsemiring (Matrix n n R)A version of Set.matrix for Subsemirings.
Given a Subsemiring S, S.matrix is the Subsemiring of square matrices m
all of whose entries m i j belong to S.
- Defined in
- Mathlib.Data.Matrix.Basic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fintypestatement and proof · cited by 7,736
- Matrixstatement and proof · cited by 4,303
- AddSubmonoidproof · cited by 1,178
- NonAssocSemiringstatement and proof · cited by 805
- Subsemiringstatement and proof · cited by 456
- AddSubmonoid.toAddSubsemigroupproof · cited by 198
- AddSubsemigroup.carrierproof · cited by 198
- Subsemiring.toAddSubmonoidproof · cited by 20
- AddSubmonoid.matrixproof · cited by 4
Cited by3
Results whose statement or proof uses this declaration.
- Subring.matrixproof · cited by 1
- Subalgebra.matrixproof · cited by 1
- Subsemiring.coe_matrixstatement and proof · cited by 0