Theorems · Theorem · linear algebra
Matrix.trace_fin_two
∀ {R : Type u_6} [inst : AddCommMonoid R] (A : Matrix (Fin 2) (Fin 2) R), A.trace = A 0 0 + A 1 1- Defined in
- Mathlib.LinearAlgebra.Matrix.Trace
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddCommMonoid
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.
- AddCommMonoidstatement and proof · cited by 12,281
- Matrixstatement and proof · cited by 4,303
- add_zeroproof · cited by 2,707
- Matrix.tracestatement · cited by 114
- Matrix.diagproof · cited by 61
Cited by13
Results whose statement or proof uses this declaration.
- isCusp_SL2Z_iffproof · cited by 3
- Matrix.GeneralLinearGroup.IsParabolic.smul_eq_self_iffproof · cited by 3
- Matrix.IsElliptic.bc_ne_zeroproof · cited by 2
- Matrix.sub_scalar_sq_eq_discrproof · cited by 2
- UpperHalfPlane.gl_smul_eq_self_iff_dist_sq_eqproof · cited by 1
- UpperHalfPlane.gl_smul_eq_self_iff_eq_fixedPtproof · cited by 1
- UpperHalfPlane.gl_smul_eq_self_iff_re_eqproof · cited by 1
- UpperHalfPlane.isElliptic_of_exists_smul_eq_selfproof · cited by 1
- Matrix.GeneralLinearGroup.IsElliptic.smul_ne_selfproof · cited by 0
- Matrix.trace_fin_two_ofproof · cited by 0
- UpperHalfPlane.exists_gl_smul_eq_self_iff_trace_eq_zeroproof · cited by 0
- UpperHalfPlane.forall_smul_eq_self_iff_mem_centerproof · cited by 0