Theorems · Theorem · group theory
AddSubgroup.vadd_apply_eq_vadd_apply_neg_vadd
∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {F : Type u_2} [inst_1 : AddGroup F] [inst_2 : AddAction F G]
[inst_3 : AddAction.QuotientAction F H] (f : F) (S : H.LeftTransversal) (q : G ⧸ H),
↑(⋯.leftQuotientEquiv q) = f +ᵥ ↑(⋯.leftQuotientEquiv (-f +ᵥ q))- Defined in
- Mathlib.GroupTheory.Complement
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Setstatement · cited by 53,352
- Equivstatement · cited by 8,337
- SetLike.coestatement · cited by 8,199
- Set.Elemstatement · cited by 7,166
- AddGroupstatement and proof · cited by 4,410
- AddSubgroupstatement and proof · cited by 3,232
- HasQuotient.Quotientstatement and proof · cited by 2,301
- HVAdd.hVAddstatement and proof · cited by 1,820
- AddActionstatement and proof · cited by 820
- AddSubgroup.IsComplementstatement · cited by 57
- vadd_neg_vaddproof · cited by 31
Cited by1
Results whose statement or proof uses this declaration.
- AddSubgroup.leftTransversals.vadd_diff_vaddproof · cited by 1