Theorems · Theorem · group theory

MulAction.IsMultiplyPreprimitive.of_bijective_map

∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {N : Type u_3} {β : Type u_4}
  [inst_2 : Group N] [inst_3 : MulAction N β] {φ : M → N} {f : α →ₑ[φ] β},
  Function.Bijective ⇑f → ∀ {n : ℕ}, MulAction.IsMultiplyPreprimitive M α n → MulAction.IsMultiplyPreprimitive N β n

Defined in: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Cited by: 1 results in Mathlib
Foundations: Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Group MulAction Group MulAction

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites29

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
Set.Elemproof · cited by 7,166
Groupstatement and proof · cited by 6,238
Set.imageproof · cited by 5,609
ENatproof · cited by 4,985
Set.preimageproof · cited by 4,946
MulActionstatement and proof · cited by 1,294
Function.Bijectivestatement and proof · cited by 863
Set.encardproof · cited by 327
Set.mem_preimageproof · cited by 190
Set.mem_imageproof · cited by 131

Cited by1

Results whose statement or proof uses this declaration.

MulAction.isMultiplyPreprimitive_congrproof · cited by 0