Theorems · Theorem · group theory
AddGroupExtension.Section.add_neg_add_add_mem_range_inl
∀ {N : Type u_1} {G : Type u_2} [inst : AddGroup N] [inst_1 : AddGroup G] {E : Type u_3} [inst_2 : AddGroup E]
{S : AddGroupExtension N E G} (σ : S.Section) (g₁ g₂ : G), -σ (g₁ + g₂) + σ g₁ + σ g₂ ∈ S.inl.range- Defined in
- Mathlib.GroupTheory.GroupExtension.Basic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 24 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
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
- AddGroupstatement and proof · cited by 4,410
- AddSubgroupstatement · cited by 3,232
- map_addproof · cited by 964
- add_assocproof · cited by 746
- map_negproof · cited by 378
- neg_add_cancelproof · cited by 256
- AddMonoidHom.rangestatement · cited by 142
- AddGroupExtensionstatement and proof · cited by 50
- AddGroupExtension.rightHomproof · cited by 28
- AddMonoidHom.mem_kerproof · cited by 26
- AddGroupExtension.inlstatement · cited by 20
Cited by1
Results whose statement or proof uses this declaration.
- AddGroupExtension.Section.exists_add_eq_add_add_inlproof · cited by 0