Theorems · Theorem · group theory
FaithfulSMul.eq_of_smul_eq_smul
∀ {M : Type u_4} {α : Type u_5} {inst : SMul M α} [self : FaithfulSMul M α] {m₁ m₂ : M},
(∀ (a : α), m₁ • a = m₂ • a) → m₁ = m₂Two elements m₁ and m₂ are equal whenever they act in the same way on all points.
- Defined in
- Mathlib.Algebra.Group.Action.Faithful
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
- Assumes
- FaithfulSMul
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- FaithfulSMulstatement and proof · cited by 340
Cited by22
Results whose statement or proof uses this declaration.
- IsGaloisGroup.card_eq_finrankproof · cited by 10
- IsGaloisGroup.of_isFractionRingproof · cited by 5
- IsGaloisGroup.of_mulEquivproof · cited by 4
- smul_left_injective'proof · cited by 3
- Module.AEval.annihilator_eq_ker_aevalproof · cited by 2
- MulSemiringAction.toAlgHom_injectiveproof · cited by 2
- IsLprojection.commuteproof · cited by 2
- IsFractionRing.faithfulSMulproof · cited by 1
- FaithfulSMul.of_injectiveproof · cited by 1
- faithfulSMul_iffproof · cited by 1
- MulAction.IwasawaStructure.isSimpleGroupproof · cited by 1
- Monoid.PushoutI.of_injectiveproof · cited by 0