Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-04 07:50 517aa8b6

View on Github →

feat(topology/algebra/star): continuity of star (#13855) This adds the obvious instances for pi, prod, units, mul_opposite, real, complex, is_R_or_C, and matrix. We already had a continuous_star lemma, but it had stronger typeclass assumptions. This resolves multiple TODO comments.

Estimated changes

modified theorem complex.continuous_conj
deleted theorem continuous.star
deleted theorem continuous_at.star
deleted theorem continuous_at_star
deleted theorem continuous_on.star
deleted theorem continuous_on_star
deleted theorem continuous_star
deleted theorem continuous_within_at.star
deleted theorem continuous_within_at_star
deleted theorem filter.tendsto.star
deleted theorem tendsto_star
modified theorem is_R_or_C.continuous_conj
added theorem continuous.star
added theorem continuous_at.star
added theorem continuous_at_star
added theorem continuous_on.star
added theorem continuous_on_star
added theorem filter.tendsto.star
added theorem tendsto_star