Theorems · Theorem · group theory

faithfulVAdd_iff_injective_vadd_zero

∀ (R : Type u_4) (A : Type u_5) [inst : AddZeroClass A] [inst_1 : VAdd R A] [VAddAssocClass R A A],
  FaithfulVAdd R A ↔ Function.Injective fun r => r +ᵥ 0

Defined in

Mathlib.Algebra.Group.Action.Faithful

Cited by

2 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

AddZeroClassVAddVAddAssocClass