Maybe these should be in mathlib

theorem Nat.totient_pow_mul_of_prime_of_dvd {p n : ℕ} (hp : Prime p) (h : p ∣ n) (m : ℕ) : (p ^ m * n).totient = p ^ m * n.totient

instance hasEnoughRootsOfUnity_two (R : Type u_1) [CommRing R] [IsDomain R] [NeZero 2] : HasEnoughRootsOfUnity R 2

theorem IsCyclic.cardinalMk_le_aleph0 (G : Type u_1) [Pow G ℤ] [IsCyclic G] : Cardinal.mk G ≤ Cardinal.aleph0

theorem IsAddCyclic.cardinalMk_le_aleph0 (G : Type u_1) [SMul ℤ G] [IsAddCyclic G] : Cardinal.mk G ≤ Cardinal.aleph0

@[simp]

theorem Padic.cardinalMk_eq_continuum (p : ℕ) [Fact (Nat.Prime p)] : Cardinal.mk ℚ_[p] = Cardinal.continuum

@[simp]

theorem PadicInt.cardinalMk_eq_continuum (p : ℕ) [Fact (Nat.Prime p)] : Cardinal.mk ℤ_[p] = Cardinal.continuum

theorem Field.isAddCyclic_iff (F : Type u_1) [Field F] : IsAddCyclic F ↔ Nat.Prime (Nat.card F)

theorem Field.not_isAddCyclic_of_infinite (F : Type u_1) [Field F] [Infinite F] : ¬IsAddCyclic F

theorem PadicInt.not_isAddCyclic (p : ℕ) [Fact (Nat.Prime p)] : ¬IsAddCyclic ℤ_[p]

def MonoidHom.equivKerProdRangeOfLeftInverse {B : Type u_1} {C : Type u_2} [CommGroup B] [Group C] (f : B →* C) (g : C →* B) (hfg : Function.LeftInverse ⇑f ⇑g) : B ≃* ↥f.ker × ↥g.range

If a surjective group homomorphism f : B →* C has a section g : C →* B, then there is a natural isomorphism of B to ker(f) × im(g). We use im(g) instead of C since if B has topology, then both of ker(f) and im(g) will also get topology automatically.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MonoidHom.val_fst_equivKerProdRangeOfLeftInverse_apply {B : Type u_1} {C : Type u_2} [CommGroup B] [Group C] (f : B →* C) (g : C →* B) (hfg : Function.LeftInverse ⇑f ⇑g) (x : B) : ↑((f.equivKerProdRangeOfLeftInverse g hfg) x).1 = x * (g (f x))⁻¹

@[simp]

theorem MonoidHom.val_snd_equivKerProdRangeOfLeftInverse_apply {B : Type u_1} {C : Type u_2} [CommGroup B] [Group C] (f : B →* C) (g : C →* B) (hfg : Function.LeftInverse ⇑f ⇑g) (x : B) : ↑((f.equivKerProdRangeOfLeftInverse g hfg) x).2 = g (f x)

@[simp]

theorem MonoidHom.equivKerProdRangeOfLeftInverse_symm_apply {B : Type u_1} {C : Type u_2} [CommGroup B] [Group C] (f : B →* C) (g : C →* B) (hfg : Function.LeftInverse ⇑f ⇑g) (x : ↥f.ker × ↥g.range) : (f.equivKerProdRangeOfLeftInverse g hfg).symm x = ↑x.1 * ↑x.2

theorem MonoidHom.continuous_equivKerProdRangeOfLeftInverse_symm {B : Type u_1} {C : Type u_2} [CommGroup B] [Group C] (f : B →* C) (g : C →* B) (hfg : Function.LeftInverse ⇑f ⇑g) [TopologicalSpace B] [ContinuousMul B] : Continuous ⇑(f.equivKerProdRangeOfLeftInverse g hfg).symm

theorem MonoidHom.continuous_equivKerProdRangeOfLeftInverse {B : Type u_1} {C : Type u_2} [CommGroup B] [Group C] (f : B →* C) (g : C →* B) (hfg : Function.LeftInverse ⇑f ⇑g) [TopologicalSpace B] [IsTopologicalGroup B] (hc : Continuous (⇑g ∘ ⇑f)) : Continuous ⇑(f.equivKerProdRangeOfLeftInverse g hfg)

def MonoidHom.continuousEquivKerProdRangeOfLeftInverse {B : Type u_1} {C : Type u_2} [CommGroup B] [Group C] (f : B →* C) (g : C →* B) (hfg : Function.LeftInverse ⇑f ⇑g) [TopologicalSpace B] [IsTopologicalGroup B] (hc : Continuous (⇑g ∘ ⇑f)) : B ≃ₜ* ↥f.ker × ↥g.range

Continuous version of equivKerProdRangeOfLeftInverse.

Equations

• f.continuousEquivKerProdRangeOfLeftInverse g hfg hc = { toMulEquiv := f.equivKerProdRangeOfLeftInverse g hfg, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem MonoidHom.val_fst_continuousEquivKerProdRangeOfLeftInverse_apply {B : Type u_1} {C : Type u_2} [CommGroup B] [Group C] (f : B →* C) (g : C →* B) (hfg : Function.LeftInverse ⇑f ⇑g) [TopologicalSpace B] [IsTopologicalGroup B] (hc : Continuous (⇑g ∘ ⇑f)) (x : B) : ↑((f.continuousEquivKerProdRangeOfLeftInverse g hfg hc) x).1 = x * (g (f x))⁻¹

@[simp]

theorem MonoidHom.val_snd_continuousEquivKerProdRangeOfLeftInverse_apply {B : Type u_1} {C : Type u_2} [CommGroup B] [Group C] (f : B →* C) (g : C →* B) (hfg : Function.LeftInverse ⇑f ⇑g) [TopologicalSpace B] [IsTopologicalGroup B] (hc : Continuous (⇑g ∘ ⇑f)) (x : B) : ↑((f.continuousEquivKerProdRangeOfLeftInverse g hfg hc) x).2 = g (f x)

@[simp]

theorem MonoidHom.continuousEquivKerProdRangeOfLeftInverse_symm_apply {B : Type u_1} {C : Type u_2} [CommGroup B] [Group C] (f : B →* C) (g : C →* B) (hfg : Function.LeftInverse ⇑f ⇑g) [TopologicalSpace B] [IsTopologicalGroup B] (hc : Continuous (⇑g ∘ ⇑f)) (x : ↥f.ker × ↥g.range) : (f.continuousEquivKerProdRangeOfLeftInverse g hfg hc).symm x = ↑x.1 * ↑x.2

instance PadicInt.isLocalHom_toZMod (p : ℕ) [Fact (Nat.Prime p)] : IsLocalHom toZMod

theorem PadicInt.zmod_cast_comp_toZModPow_eq_toZMod (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) (h : n ≠ 0) : (ZMod.castHom ⋯ (ZMod p)).comp (toZModPow n) = toZMod

instance PadicInt.isLocalHom_toZModPow (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) [NeZero n] : IsLocalHom (toZModPow n)

theorem PadicInt.unitsMap_toZMod_surjective (p : ℕ) [Fact (Nat.Prime p)] : Function.Surjective ⇑(Units.map ↑toZMod)

theorem PadicInt.unitsMap_toZModPow_surjective (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : Function.Surjective ⇑(Units.map ↑(toZModPow n))

Some silly results for ZMod

theorem ZMod.units_eq_one_of_eq_two {q : ℕ} (hq : q = 2) (x : (ZMod q)ˣ) : x = 1

theorem ZMod.units_eq_one_or_neg_one_of_eq_three {q : ℕ} (hq : q = 3) (x : (ZMod q)ˣ) : x = 1 ∨ x = -1

theorem ZMod.units_eq_one_or_neg_one_of_eq_four {q : ℕ} (hq : q = 4) (x : (ZMod q)ˣ) : x = 1 ∨ x = -1

theorem ZMod.units_eq_one_or_neg_one_of_eq_six {q : ℕ} (hq : q = 6) (x : (ZMod q)ˣ) : x = 1 ∨ x = -1

theorem ZMod.eq_one_of_eq_two_of_isUnit {q : ℕ} (hq : q = 2) (x : ZMod q) (hx : IsUnit x) : x = 1

theorem ZMod.eq_one_or_neg_one_of_eq_three_of_isUnit {q : ℕ} (hq : q = 3) (x : ZMod q) (hx : IsUnit x) : x = 1 ∨ x = -1

theorem ZMod.eq_one_or_neg_one_of_eq_four_of_isUnit {q : ℕ} (hq : q = 4) (x : ZMod q) (hx : IsUnit x) : x = 1 ∨ x = -1

theorem ZMod.eq_one_or_neg_one_of_eq_six_of_isUnit {q : ℕ} (hq : q = 6) (x : ZMod q) (hx : IsUnit x) : x = 1 ∨ x = -1