Theorems · Theorem · group theory
one_smul
∀ (M : Type u_1) {α : Type u_5} [inst : Monoid M] [inst_1 : MulAction M α] (b : α), 1 • b = b- Defined in
- Mathlib.Algebra.Group.Action.Defs
- Cited by
- 1,374 results in Mathlib
- Foundations
- Depth 7 from the axioms, rests on 33 definitions · uses no axioms
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.
- Monoidstatement and proof · cited by 3,887
- MulActionstatement and proof · cited by 1,294
- MulAction.one_smulproof · cited by 1
Cited by1,375
Results whose statement or proof uses this declaration.
- Nat.cast_smul_eq_nsmulproof · cited by 110
- IsScalarTower.algebraMap_eqproof · cited by 110
- inv_smul_smulproof · cited by 76
- Submodule.mem_span_singletonproof · cited by 61
- two_smulproof · cited by 57
- smul_inv_smulproof · cited by 53
- LinearMap.toMatrix_applyproof · cited by 52
- smul_one_smulproof · cited by 43
- SMulCommClass.of_commMonoidproof · cited by 42
- AffineMap.lineMap_apply_oneproof · cited by 37
- Convex.combo_selfproof · cited by 29
- Int.cast_smul_eq_zsmulproof · cited by 28
Showing the 200 most cited of 1,375.