Commit 2025-02-16 15:19 55674a09

View on Github →

chore: rename Topological(Semi)Ring -> IsTopological(Semi)Ring and Topological(Add)Group -> IsTopological(Add)Group (#21472)

Estimated changes

modified theorem AmpleSet.of_one_lt_codim
modified theorem IsCompactOperator.sub
modified theorem separate_convex_open_set
modified theorem Seminorm.continuous_of_le
modified theorem CFC.rpow_neg
modified theorem CFC.rpow_rpow
modified theorem ProfiniteGrp.coe_of
modified structure GroupTopology
added theorem IsTopologicalGroup.ext
deleted theorem TopologicalGroup.ext
deleted theorem TopologicalGroup.ext_iff
deleted theorem TopologicalGroup.t1Space
modified theorem topologicalGroup_inf
modified theorem topologicalGroup_quotient
modified theorem IsOpenUnits.of_isAdic
modified theorem ContinuousSMul.of_nhds_zero
modified theorem Ideal.isCompact_of_fg
modified theorem unique_topology_of_t2
modified theorem isAdic_iff
modified theorem is_bot_adic_iff
deleted theorem TopologicalRing.of_norm
modified theorem continuousAt_fract
modified theorem continuousOn_fract
modified theorem tendsto_fract_left'
modified theorem tendsto_fract_left
modified theorem tendsto_fract_right'
modified theorem tendsto_fract_right
modified structure RingTopology
modified theorem SeparationQuotient.mk_zpow
modified theorem TopCommRingCat.coe_of
modified theorem ContinuousMap.coe_zpow
modified theorem ContinuousMap.zpow_apply
modified theorem ContinuousMap.zpow_comp
modified theorem Continuous.matrix_adjugate
modified theorem Continuous.matrix_cramer
modified theorem Continuous.matrix_det
modified theorem continuousAt_matrix_inv