Commit 2023-09-12 22:27 e36d25ef

View on Github →

chore: fix port of surjective_quotient_mk (#7096) The mathlib3 lemma is about quotient.mk, which takes an instance argument and is translated into mathlib4 as Quotient.mk'.

Estimated changes

Modified Mathlib/Data/Fintype/Card.lean

Modified Mathlib/Data/Quot.lean

added theorem surjective_quotient_mk'

deleted theorem surjective_quotient_mk

Modified Mathlib/Data/Real/CauSeqCompletion.lean

Modified Mathlib/Data/Setoid/Basic.lean

Modified Mathlib/Data/Sym/Sym2.lean

Modified Mathlib/MeasureTheory/Constructions/Polish.lean

Modified Mathlib/Topology/Connected.lean

Modified Mathlib/Topology/PathConnected.lean

Modified Mathlib/Topology/UniformSpace/Completion.lean