LeanPool.OrderPQ.MonoidHom

theorem Set.nat_card_range_of_injective {α : Type u_1} {β : Type u_2} (f : α → β) (hf : Function.Injective f) : Nat.card ↑(range f) = Nat.card α

theorem MonoidHom.nat_card_range_of_injective {α : Type u_1} {β : Type u_2} [Group α] [Group β] {f : α →* β} (hf : Function.Injective ⇑f) : Nat.card ↥f.range = Nat.card α

theorem AddMonoidHom.nat_card_range_of_injective {α : Type u_1} {β : Type u_2} [AddGroup α] [AddGroup β] {f : α →+ β} (hf : Function.Injective ⇑f) : Nat.card ↥f.range = Nat.card α

theorem zpow_eq_self_iff_modEq {α : Type u_1} [Group α] {x : α} {n : ℤ} : x ^ n = x ↔ n ≡ 1 [ZMOD ↑(orderOf x)]

theorem zsmul_eq_self_iff_modEq {α : Type u_1} [AddGroup α] {x : α} {n : ℤ} : n • x = x ↔ n ≡ 1 [ZMOD ↑(addOrderOf x)]

theorem Int.modEq_of_modEq_dvd {n m a b : ℤ} (h : m ∣ n) : a ≡ b [ZMOD n] → a ≡ b [ZMOD m]

theorem Subgroup.nat_card_top {α : Type u_1} [Group α] : Nat.card ↥⊤ = Nat.card α

theorem AddSubgroup.nat_card_top {α : Type u_1} [AddGroup α] : Nat.card ↥⊤ = Nat.card α

theorem MonoidHom.eq_of_apply_eq {α : Type u_1} {β : Type u_2} [Group α] [Group β] {x : α} (hx : ∀ (a : α), a ∈ Subgroup.zpowers x) (f₁ f₂ : α →* β) (h2 : f₁ x = f₂ x) : f₁ = f₂

theorem AddMonoidHom.eq_of_apply_eq {α : Type u_1} {β : Type u_2} [AddGroup α] [AddGroup β] {x : α} (hx : ∀ (a : α), a ∈ AddSubgroup.zmultiples x) (f₁ f₂ : α →+ β) (h2 : f₁ x = f₂ x) : f₁ = f₂

theorem MulEquiv.eq_of_apply_eq {α : Type u_1} {β : Type u_2} [Group α] [Group β] {x : α} (hx : ∀ (a : α), a ∈ Subgroup.zpowers x) (f₁ f₂ : α ≃* β) (h2 : f₁ x = f₂ x) : f₁ = f₂

theorem AddEquiv.eq_of_apply_eq {α : Type u_1} {β : Type u_2} [AddGroup α] [AddGroup β] {x : α} (hx : ∀ (a : α), a ∈ AddSubgroup.zmultiples x) (f₁ f₂ : α ≃+ β) (h2 : f₁ x = f₂ x) : f₁ = f₂

theorem MonoidHom.exists_of_generator_and_image {α : Type u_1} {β : Type u_2} [Group α] [Group β] {x : α} (hx : ∀ (a : α), a ∈ Subgroup.zpowers x) {y : β} (hy : orderOf y ∣ Nat.card α) : ∃ (f : α →* β), f x = y

theorem AddMonoidHom.exists_of_generator_and_image {α : Type u_1} {β : Type u_2} [AddGroup α] [AddGroup β] {x : α} (hx : ∀ (a : α), a ∈ AddSubgroup.zmultiples x) {y : β} (hy : addOrderOf y ∣ Nat.card α) : ∃ (f : α →+ β), f x = y