Theorems · Theorem · group theory
AddAction.isPreprimitive_congr
∀ {M : Type u_3} [inst : AddGroup M] {α : Type u_4} [inst_1 : AddAction M α] {N : Type u_5} {β : Type u_6}
[inst_2 : AddGroup N] [inst_3 : AddAction N β] {φ : M → N} {f : α →ₑ[φ] β},
Function.Surjective φ → Function.Bijective ⇑f → (AddAction.IsPreprimitive M α ↔ AddAction.IsPreprimitive N β)- Cited by
- 4 results in Mathlib
- Foundations
- Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites18
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
- Setproof · cited by 53,352
- AddGroupstatement and proof · cited by 4,410
- Function.Bijectivestatement and proof · cited by 863
- AddActionstatement and proof · cited by 820
- Function.Bijective.injectiveproof · cited by 115
- Function.Bijective.surjectiveproof · cited by 114
- Set.preimage_image_eqproof · cited by 87
- AddActionHomstatement and proof · cited by 82
- AddAction.IsBlockproof · cited by 65
- AddAction.IsPretransitiveproof · cited by 56
- AddAction.IsPreprimitivestatement and proof · cited by 25
Cited by4
Results whose statement or proof uses this declaration.
- AddAction.isPreprimitive_ofFixingAddSubgroup_addConj_iffproof · cited by 1
- AddAction.isPreprimitive_of_fixingAddSubgroup_empty_iffproof · cited by 1
- AddAction.isPreprimitive_fixingAddSubgroup_insert_iffproof · cited by 1
- AddAction.isMultiplyPreprimitive_congrproof · cited by 0