Commit 2026-06-10 13:50 5daf17f4

View on Github →

chore(Topology/Covering/Quotient): automated extraction (#40467) This PR was automatically created from PR #33108 by @alreadydone via a review comment by @ocfnash.

Estimated changes

Modified Mathlib/Topology/Covering/Quotient.lean

added theorem IsQuotientCoveringMap.coe_mulActionFiber_smul

added theorem IsQuotientCoveringMap.exists_toPermFiber_eq

added theorem IsQuotientCoveringMap.fiberEquivGroup_eq_iff

added theorem IsQuotientCoveringMap.fiberEquivGroup_self

added theorem IsQuotientCoveringMap.fiberEquivGroup_smul_self

modified theorem IsQuotientCoveringMap.homeomorph_comp

modified theorem IsQuotientCoveringMap.isCancelSMul

added def IsQuotientCoveringMap.mulActionFiber

added theorem IsQuotientCoveringMap.mulActionFiber_isPretransitive

added def IsQuotientCoveringMap.toPermFiber

added theorem IsQuotientCoveringMap.toPermFiber_ext

added theorem IsQuotientCoveringMap.toPermFiber_injective