ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I : Submodule R A
⊢ ∀ (m : A), m ∈ I → ∀ (n : A), n ∈ 1 / I → m * n ∈ 1
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I : Submodule R A
⊢ I * (1 / I) ≤ 1
rw [Submodule.mul_le]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m✝ n✝ : A
I : Submodule R A
m : A
hm : m ∈ I
n : A
hn : n ∈ 1 / I
⊢ m * n ∈ 1
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I : Submodule R A
⊢ ∀ (m : A), m ∈ I → ∀ (n : A), n ∈ 1 / I → m * n ∈ 1
intro m hm n hn
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m✝ n✝ : A
I : Submodule R A
m : A
hm : m ∈ I
n : A
hn : ∀ (y : A), y ∈ I → n * y ∈ 1
⊢ m * n ∈ 1
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m✝ n✝ : A
I : Submodule R A
m : A
hm : m ∈ I
n : A
hn : n ∈ 1 / I
⊢ m * n ∈ 1
rw [Submodule.mem_div_iff_forall_mul_mem] at hn
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m✝ n✝ : A
I : Submodule R A
m : A
hm : m ∈ I
n : A
hn : ∀ (y : A), y ∈ I → n * y ∈ 1
⊢ n * m ∈ 1
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m✝ n✝ : A
I : Submodule R A
m : A
hm : m ∈ I
n : A
hn : ∀ (y : A), y ∈ I → n * y ∈ 1
⊢ m * n ∈ 1
rw [mul_comm]
no goals
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m✝ n✝ : A
I : Submodule R A
m : A
hm : m ∈ I
n : A
hn : ∀ (y : A), y ∈ I → n * y ∈ 1
⊢ n * m ∈ 1
exact hn m hm