should this be an instance

Stream: general

[Johan Commelin]

At the end of algebra.module there are the following lines:

namespace submodule

variables {R:discrete_field α} [add_comm_group β] [add_comm_group γ]
variables [vector_space α β] [vector_space α γ]
variables (p p' : submodule α β)
variables {r : α} {x y : β}
include R

theorem smul_mem_iff (r0 : r ≠ 0) : r • x ∈ p ↔ x ∈ p :=
⟨λ h, by simpa [smul_smul, inv_mul_cancel r0] using p.smul_mem (r⁻¹) h,
 p.smul_mem r⟩

end submodule

Note that it says variables {R:discrete_field α}. Shouldn't that be [R : discrete_field α]?

[Kenny Lau]

that should be something I missed in the second module refactor

[Johan Commelin]

Ok, I'll fix it.