Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-29 12:25 b2e0a2d0

View on Github →

feat(group_theory/subgroup/basic): inclusion lemmas (#13754) A few lemmas for set.inclusion, subgroup.inclusion, subalgebra.inclusion.

Estimated changes

modified theorem subalgebra.inclusion_right
modified theorem set.coe_inclusion
modified def set.inclusion
modified theorem set.inclusion_inclusion
modified theorem set.inclusion_injective
added theorem set.inclusion_mk
modified theorem set.inclusion_right
modified theorem set.inclusion_self
modified theorem set.range_inclusion