English
Dividing by a spanSingleton equals multiplying by its inverse spanSingleton.
Русский
Разделение на spanSingleton эквивалентно умножению на обратный spanSingleton.
LaTeX
$$J / spanSingleton R⁰ d = spanSingleton R⁰ d⁻¹ * J$$
Lean4
@[simp]
theorem div_spanSingleton (J : FractionalIdeal R₁⁰ K) (d : K) : J / spanSingleton R₁⁰ d = spanSingleton R₁⁰ d⁻¹ * J :=
by
rw [← one_div_spanSingleton]
by_cases hd : d = 0
· simp only [hd, spanSingleton_zero, div_zero, zero_mul]
have h_spand : spanSingleton R₁⁰ d ≠ 0 := mt spanSingleton_eq_zero_iff.mp hd
apply le_antisymm
· intro x hx
dsimp only [val_eq_coe] at hx
⊢ -- Porting note: get rid of the partially applied `coe`s
rw [coe_div h_spand, Submodule.mem_div_iff_forall_mul_mem] at hx
specialize hx d (mem_spanSingleton_self R₁⁰ d)
have h_xd : x = d⁻¹ * (x * d) := by field_simp
rw [coe_mul, one_div_spanSingleton, h_xd]
exact Submodule.mul_mem_mul (mem_spanSingleton_self R₁⁰ _) hx
·
rw [le_div_iff_mul_le h_spand, mul_assoc, mul_left_comm, one_div_spanSingleton, spanSingleton_mul_spanSingleton,
inv_mul_cancel₀ hd, spanSingleton_one, mul_one]
