KummerTheory.dense_torsion_pi_of_finite
The torsion elements are dense in an arbitrary product of finite commutative groups.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
noncomputable section
namespace KummerTheory
open LocalFieldTheory.PadicLean source · statement
theorem dense_torsion_pi_of_finite
{ι : Type*} (G : ι → Type*)
[(i : ι) → CommGroup (G i)]
[(i : ι) → TopologicalSpace (G i)]
[(i : ι) → Finite (G i)] :
Dense
(CommGroup.torsion ((i : ι) → G i) :
Set ((i : ι) → G i))