Theorems · Theorem · group theory
IsCentralScalar.op_smul_eq_smul
∀ {M : Type u_9} {α : Type u_10} {inst : SMul M α} {inst_1 : SMul Mᵐᵒᵖ α} [self : IsCentralScalar M α] (m : M) (a : α),
MulOpposite.op m • a = m • aThe right and left actions of M on α are equal.
- Defined in
- Mathlib.Algebra.Group.Action.Defs
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
- Assumes
- IsCentralScalar
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MulOppositestatement and proof · cited by 1,135
- MulOpposite.opstatement · cited by 520
- IsCentralScalarstatement and proof · cited by 39
Cited by22
Results whose statement or proof uses this declaration.
- dotProduct_toMatrix₂_mulVecproof · cited by 2
- TrivSqZeroExt.exp_defproof · cited by 2
- IsCentralScalar.unop_smul_eq_smulproof · cited by 2
- OnePoint.smul_some_eq_iteproof · cited by 2
- apply_eq_dotProduct_toMatrix₂_mulVecproof · cited by 2
- Matrix.permMatrix_mulVecproof · cited by 1
- Matrix.maxGenEigenspace_toLin_diagonal_eq_eigenspaceproof · cited by 1
- OnePoint.smul_infty_defproof · cited by 1
- Matrix.lt_two_mul_of_mul_diagonal_posDef_of_for_le_of_hasEigenproof · cited by 1
- hasStrictFDerivAt_list_prodproof · cited by 1
- Matrix.inner_toEuclideanCLMproof · cited by 1
- FunLike.isCentralScalarproof · cited by 0