Theorems · Inductive type · group theory
FaithfulSMul
(M : Type u_4) → (α : Type u_5) → [SMul M α] → Prop
Typeclass for faithful actions.
- Defined in
- Mathlib.Algebra.Group.Action.Faithful
- Cited by
- 340 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- SMul
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by385
Results whose statement or proof uses this declaration.
- FaithfulSMul.algebraMap_injectivestatement and proof · cited by 198
- FractionRing.liftAlgebrastatement and proof · cited by 43
- RootPairing.posRootFormstatement and proof · cited by 23
- FaithfulSMul.eq_of_smul_eq_smulstatement and proof · cited by 22
- RootPairing.RootPositiveForm.posFormstatement and proof · cited by 22
- AlgebraicIndependent.matroidstatement and proof · cited by 17
- faithfulSMul_iff_algebraMap_injectivestatement · cited by 17
- RatFunc.liftAlgebrastatement and proof · cited by 15
- RootPairing.RootFormInstatement and proof · cited by 13
- LinearIndependent.restrict_scalars'statement and proof · cited by 12
- RootPairing.PolarizationInstatement and proof · cited by 12
- RootPairing.coroot'Instatement and proof · cited by 12
Showing the 200 most cited of 385.