Theorems · Theorem · linear algebra
Matrix.single_neg
∀ {n : Type u_3} {α : Type u_7} [inst : DecidableEq n] [inst_1 : NegZeroClass α] (i j : n) (b : α),
-Matrix.single i j b = Matrix.single i j (-b)- Defined in
- Mathlib.Data.Matrix.Basis
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext, Quot.sound
- Assumes
- DecidableEqNegZeroClass
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Matrixstatement · cited by 4,303
- neg_zeroproof · cited by 542
- Matrix.extproof · cited by 540
- Matrix.singlestatement · cited by 129
- NegZeroClassstatement and proof · cited by 23
- Matrix.neg_ofproof · cited by 1
- neg_iteproof · cited by 1
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.