Theorems · Theorem · group theory
AddAction.bijective
∀ {α : Type u_5} {β : Type u_6} [inst : AddGroup α] [inst_1 : AddAction α β] (g : α), Function.Bijective fun x => g +ᵥ x- Defined in
- Mathlib.Algebra.Group.Action.Basic
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddGroupstatement and proof · cited by 4,410
- HVAdd.hVAddstatement · cited by 1,820
- Function.Bijectivestatement · cited by 863
- AddActionstatement and proof · cited by 820
- Equiv.bijectiveproof · cited by 132
- AddAction.toPermproof · cited by 21
Cited by6
Results whose statement or proof uses this declaration.
- AddAction.injectiveproof · cited by 24
- AddAction.surjectiveproof · cited by 4
- MeasureTheory.Measure.pairwise_aedisjoint_of_aedisjoint_forall_ne_zeroproof · cited by 2
- Set.vadd_set_piproof · cited by 1
- IsAddUnit.vadd_bijectiveproof · cited by 1
- Set.vadd_set_iInterproof · cited by 1