Commit 2023-03-03 08:27 3155a57a

View on Github →

feat: add units.embedding_val₀ (#2590) Forward-port #18536

Estimated changes

Modified Mathlib/GroupTheory/Index.lean

Modified Mathlib/GroupTheory/Subgroup/Basic.lean

modified theorem div_mem_comm_iff

modified theorem inv_mem_iff

Modified Mathlib/GroupTheory/Subgroup/Pointwise.lean

modified theorem inv_coe_set

Modified Mathlib/Topology/Algebra/Constructions.lean

added theorem Units.embedding_val_mk

added theorem Units.topology_eq_inf

Modified Mathlib/Topology/Algebra/Group/Basic.lean

added theorem Units.embedding_val

added def toUnits_homeomorph

Modified Mathlib/Topology/Algebra/GroupWithZero.lean

added theorem Units.embedding_val₀