IndisputableMonolith.Gap45.AddGroupView

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Gap45
   5namespace AddGroupView
   6
   7open Nat
   8
   9/-- Additive version: if `(8) • a = 0` and `(45) • a = 0`, then the additive order of `a`
  10divides `gcd(8,45)=1`, hence `a = 0`. -/
  11lemma trivial_intersection_nsmul {A : Type*} [AddGroup A] {a : A}
  12  (h8 : (8 : ℕ) • a = 0) (h45 : (45 : ℕ) • a = 0) : a = 0 := by
  13  have h8d : addOrderOf a ∣ 8 := (addOrderOf_dvd_iff_nsmul_eq_zero (a:=a) (n:=8)).2 h8
  14  have h45d : addOrderOf a ∣ 45 := (addOrderOf_dvd_iff_nsmul_eq_zero (a:=a) (n:=45)).2 h45
  15  have hgcd : addOrderOf a ∣ Nat.gcd 8 45 := Nat.dvd_gcd h8d h45d
  16  have hone : addOrderOf a ∣ 1 := by simpa using hgcd
  17  have h1 : addOrderOf a = 1 := Nat.dvd_one.mp hone
  18  simpa [h1] using (addOrderOf_eq_one_iff.mpr rfl)
  19
  20end AddGroupView
  21end Gap45
  22end IndisputableMonolith
  23