Theorems · Inductive type · group theory
FaithfulVAdd
(G : Type u_4) → (P : Type u_5) → [VAdd G P] → Prop
Typeclass for faithful actions.
- Defined in
- Mathlib.Algebra.Group.Action.Faithful
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- VAdd
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.
- VAddstatement · cited by 616
Cited by19
Results whose statement or proof uses this declaration.
- FaithfulVAdd.eq_of_vadd_eq_vaddstatement and proof · cited by 5
- vadd_left_injective'statement and proof · cited by 3
- faithfulVAdd_iff_injective_vadd_zerostatement and proof · cited by 2
- AddAction.toPerm_injectivestatement and proof · cited by 1
- AddAction.fixedBy_eq_univ_iff_eq_zerostatement and proof · cited by 1
- faithfulVAdd_iffstatement and proof · cited by 1
- AddAut.apply_faithfulSMulstatement · cited by 0
- AddLeftCancelMonoid.to_faithfulVAdd_addOppositestatement · cited by 0
- AddRightCancelMonoid.faithfulVAddstatement · cited by 0
- Equiv.faithfulVAddstatement and proof · cited by 0
- VAddAssocClass.to₁₂₃statement and proof · cited by 0
- FaithfulVAdd.casesOnstatement and proof · cited by 0