Theorems · Theorem · group theory

AddSubgroup.closure_le

∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) {k : Set G}, AddSubgroup.closure k ≤ K ↔ k ⊆ ↑K

An additive subgroup K includes closure k if and only if it includes k

Defined in

Mathlib.Algebra.Group.Subgroup.Lattice

Cited by

30 results in Mathlib

Foundations

Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddGroup