Commit 2023-05-12 02:52 c01ced8c

View on Github →

feat: port Analysis.NormedSpace.Units (#3856)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/GroupWithZero/Units/Basic.lean

Created Mathlib/Analysis/NormedSpace/Units.lean

added theorem Ideal.IsMaximal.closure_eq

added theorem Ideal.closure_ne_top

added theorem Ideal.eq_top_of_norm_lt_one

added theorem NormedRing.inverse_add

added theorem NormedRing.inverse_add_norm

added theorem NormedRing.inverse_add_norm_diff_first_order

added theorem NormedRing.inverse_add_norm_diff_nth_order

added theorem NormedRing.inverse_add_norm_diff_second_order

added theorem NormedRing.inverse_add_nth_order

added theorem NormedRing.inverse_continuousAt

added theorem NormedRing.inverse_one_sub

added theorem NormedRing.inverse_one_sub_norm

added theorem NormedRing.inverse_one_sub_nth_order'

added theorem NormedRing.inverse_one_sub_nth_order

added def Units.add

added theorem Units.isOpenMap_val

added def Units.ofNearby

added def Units.oneSub

added theorem Units.openEmbedding_val

added theorem nonunits.subset_compl_ball

Modified Mathlib/Topology/Algebra/Constructions.lean

added theorem Units.embedding_val_mk'