Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-04 08:32 0d249d70

View on Github →

feat(analysis/normed_space/*): group of units of a normed ring is open (#3210) In a complete normed ring, the group of units is an open subset of the ring (Zulip) Supporting material:

  • topology.metric_space.basic, analysis.normed_space.basic, normed_space.operator_norm: some lemmas about limits and infinite sums in metric and normed spaces
  • analysis.normed_space.basic, normed_space.operator_norm: left- and right- multiplication in a normed ring (algebra) is a bounded homomorphism (linear map); the algebra/linear-map versions are not needed for the main result but included for completeness
  • analysis.normed_space.basic: a normed algebra is nonzero (not needed for the main result) (Zulip)
  • algebra.group_with_zero: the subsingleton_or_nonzero dichotomy for monoids with zero (Zulip) (written by @jcommelin )
  • analysis.specific_limits: results on geometric series in a complete normed_ring; relies on
  • algebra.geom_sum: "left" variants of some existing "right" lemmas on finite geometric series; relies on
  • algebra.opposites, algebra.group_power, algebra.big_operators: lemmas about the opposite ring (Zulip)

Estimated changes

added theorem with_top.op_sum
added theorem with_top.unop_sum
added theorem mul_geom_sum
added theorem mul_neg_geom_sum
added theorem op_geom_series
added theorem units.op_pow
added theorem units.unop_pow
added theorem opposite.op_sub
added theorem opposite.unop_sub
added theorem eventually_norm_pow_le
added theorem mul_left_bound
added theorem mul_right_bound
added theorem squeeze_zero_norm'
added theorem squeeze_zero_norm
added theorem units.norm_pos
added def units.add
added theorem units.add_coe
added theorem units.is_open
added def units.one_sub
added theorem units.one_sub_coe
added theorem geom_series_mul_neg
added theorem mul_neg_geom_series
added theorem squeeze_zero'