FormalConjecturesForMathlib/Topology/Algebra/InfiniteSum/Group.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 2 files
  1. lemma Multipliable.tendsto_tprod_one line 29 source

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

    Statement uses: CommGroup, TopologicalSpace, IsTopologicalGroup, Filter, Set, Multipliable, SummationFilter.unconditional, Filter.Eventually, Not, Membership.mem, Filter.Tendsto, tprod, nhds, OfNat.ofNat

    Proof uses: Eq.mpr, id, Eq, congrArg, propext, Filter.tendsto_iff_eventually, Finset, Disjoint, Set.ofPred, Exists, Multipliable.tprod_vanishing, Filter.mp_mem, Iff.mpr, Finset.eventually_all, Filter.univ_mem', Eq.trans, forall_congr, implies_congr, Eq.refl

    45 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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