Theorems · Theorem · group theory
faithfulSMul_iff_injective_smul_one
∀ (R : Type u_4) (A : Type u_5) [inst : MulOneClass A] [inst_1 : SMul R A] [IsScalarTower R A A], FaithfulSMul R A ↔ Function.Injective fun r => r • 1
- Defined in
- Mathlib.Algebra.Group.Action.Faithful
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses no axioms
- Assumes
- MulOneClassSMulIsScalarTower
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.
- IsScalarTowerstatement and proof · cited by 3,896
- one_mulproof · cited by 2,841
- MulOneClassstatement and proof · cited by 1,018
- FaithfulSMulstatement and proof · cited by 340
- smul_mul_assocproof · cited by 77
Cited by8
Results whose statement or proof uses this declaration.
- faithfulSMul_iff_algebraMap_injectiveproof · cited by 17
- LinearIndependent.restrict_scalars'proof · cited by 12
- FaithfulSMul.transproof · cited by 6
- LinearIndependent.iff_fractionRingproof · cited by 3
- Module.lift_rank_bot_le_lift_rank_of_isScalarTowerproof · cited by 2
- NeZero.of_faithfulSMulproof · cited by 2
- FaithfulSMul.tower_botproof · cited by 1
- Submodule.ker_unitsToPicproof · cited by 1