FLT/Mathlib/Topology/Algebra/Group/Units.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Units

Material destined for Mathlib.

Imports (3)
Imported by 2 files
  1. lemma Submonoid.units_isOpen line 20 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: TopologicalSpace, Monoid, Submonoid, IsOpen, Units, Subgroup, Submonoid.units

    Proof uses: IsOpen.inter, Set.preimage, Inv.inv, Submonoid.inv, Submonoid.comap, MonoidHom, Units.coeHom, IsOpen.preimage, Units.continuous_val, Units.continuous_coe_inv

    19 instances, coercions and auxiliary constants left out.