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

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Quotient

Material destined for Mathlib.

Imports (2)
Imported by 3 files
  1. def QuotientGroup.continuousMulEquiv line 23 source

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

    Statement uses: Group, Subgroup, Subgroup.Normal, TopologicalSpace, ContinuousMulEquiv, Eq, Subgroup.map, HasQuotient.Quotient

    Proof uses: MulEquiv, QuotientGroup.congr, ContinuousMulEquiv.mk

    29 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

    Open to load the checked before-and-after goal states.

  2. theorem QuotientGroup.isOpenQuotientMap_rightrel_mk line 38 source

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

    Statement uses: Group, TopologicalSpace, ContinuousMul, Subgroup, IsOpenQuotientMap, Quot, QuotientGroup.rightRel, Quot.mk

    Proof uses: IsOpenQuotientMap.mk, Quot.mk_surjective, continuous_quot_mk, isOpenMap_quotient_mk'_mul, Subtype, Membership.mem

    28 instances, coercions and auxiliary constants left out.