ValueGroup.lean

theorem int_lcm_dvd_iff_dvd_and_dvd (d e n : ℤ) :
    ((d.lcm e : ℕ) : ℤ) ∣ n ↔ d ∣ n ∧ e ∣ n

theorem int_lcm_dvd_of_dvd_of_dvd {d e n : ℤ}
    (hd : d ∣ n) (he : e ∣ n) :
    ((d.lcm e : ℕ) : ℤ) ∣ n

theorem integerMultipleSubgroup_lcm_eq_inf (d e : ℤ) :
    integerMultipleSubgroup ((d.lcm e : ℕ) : ℤ) =
      integerMultipleSubgroup d ⊓ integerMultipleSubgroup e

theorem integerMultipleSubgroup_le_iff_dvd (a b : ℤ) :
    integerMultipleSubgroup b ≤ integerMultipleSubgroup a ↔ a ∣ b

theorem int_lcm_dvd_of_integerMultipleSubgroup_le_of_le
    {n d e : ℤ}
    (hd : integerMultipleSubgroup n ≤ integerMultipleSubgroup d)
    (he : integerMultipleSubgroup n ≤ integerMultipleSubgroup e) :
    ((d.lcm e : ℕ) : ℤ) ∣ n

def subgroupValueSubgroup
    (V : MultiplicativeIntegerValuation G) (S : Subgroup G) :
    Subgroup (Multiplicative ℤ) where
  carrier := {n | ∃ x : G, x ∈ S ∧ V.valuationHom x = n}
  one_mem' := ⟨1, S.one_mem, V.valuationHom.map_one⟩
  mul_mem' := by
    rintro a b ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩
    exact ⟨x * y, S.mul_mem hx hy, V.valuationHom.map_mul x y⟩
  inv_mem' := by
    rintro a ⟨x, hx, rfl⟩
    exact ⟨x⁻¹, S.inv_mem hx, V.valuationHom.map_inv x⟩

theorem mem_subgroupValueSubgroup_iff
    (V : MultiplicativeIntegerValuation G) (S : Subgroup G)
    (n : Multiplicative ℤ) :
    n ∈ V.subgroupValueSubgroup S ↔
      ∃ x : G, x ∈ S ∧ V.valuationHom x = n

theorem ofAdd_mem_subgroupValueSubgroup_iff
    (V : MultiplicativeIntegerValuation G) (S : Subgroup G) (n : ℤ) :
    Multiplicative.ofAdd n ∈ V.subgroupValueSubgroup S ↔
      ∃ x : G, x ∈ S ∧ V.val x = n

theorem subgroupValueSubgroup_mono
    (V : MultiplicativeIntegerValuation G) {S T : Subgroup G}
    (hST : S ≤ T) :
    V.subgroupValueSubgroup S ≤ V.subgroupValueSubgroup T

theorem subgroupValueSubgroup_le_integerMultipleSubgroup_iff
    (V : MultiplicativeIntegerValuation G) (S : Subgroup G) (d : ℤ) :
    V.subgroupValueSubgroup S ≤ integerMultipleSubgroup d ↔
      ∀ x : G, x ∈ S → d ∣ V.val x

theorem subgroupValueSubgroup_le_integerMultipleSubgroup_of_le
    (V : MultiplicativeIntegerValuation G) {S T : Subgroup G} {d : ℤ}
    (hST : S ≤ T)
    (hT : V.subgroupValueSubgroup T ≤ integerMultipleSubgroup d) :
    V.subgroupValueSubgroup S ≤ integerMultipleSubgroup d

theorem integerMultipleSubgroup_le_subgroupValueSubgroup_of_exists_mem_val
    (V : MultiplicativeIntegerValuation G) {S : Subgroup G} {n : ℤ}
    (hn : ∃ x : G, x ∈ S ∧ V.val x = n) :
    integerMultipleSubgroup n ≤ V.subgroupValueSubgroup S

theorem int_lcm_dvd_of_exists_mem_val_of_subgroupValueSubgroup_le
    (V : MultiplicativeIntegerValuation G) {S : Subgroup G} {n d e : ℤ}
    (hn : ∃ x : G, x ∈ S ∧ V.val x = n)
    (hd : V.subgroupValueSubgroup S ≤ integerMultipleSubgroup d)
    (he : V.subgroupValueSubgroup S ≤ integerMultipleSubgroup e) :
    ((d.lcm e : ℕ) : ℤ) ∣ n

theorem int_lcm_dvd_of_exists_mem_val_of_le_of_subgroupValueSubgroup_le
    (V : MultiplicativeIntegerValuation G) {S T : Subgroup G} {n d e : ℤ}
    (hn : ∃ x : G, x ∈ S ∧ V.val x = n)
    (hST : S ≤ T)
    (hd : V.subgroupValueSubgroup T ≤ integerMultipleSubgroup d)
    (he : V.subgroupValueSubgroup T ≤ integerMultipleSubgroup e) :
    ((d.lcm e : ℕ) : ℤ) ∣ n