Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-16 08:37 1181c990

View on Github →

feat(algebra/order/archimedean): upgrade some ∃ to ∃! (#10343)

Estimated changes

Modified src/algebra/order/archimedean.lean

deleted theorem exists_add_int_smul_mem_Ico

deleted theorem exists_add_int_smul_mem_Ioc

deleted theorem exists_int_smul_near_of_pos'

deleted theorem exists_int_smul_near_of_pos

added theorem exists_unique_add_zsmul_mem_Ico

added theorem exists_unique_add_zsmul_mem_Ioc

added theorem exists_unique_zsmul_near_of_pos'

added theorem exists_unique_zsmul_near_of_pos

Modified src/algebra/periodic.lean

Modified src/group_theory/archimedean.lean

Modified src/logic/function/basic.lean

deleted theorem function.bijective.exists_unique

added theorem function.bijective.exists_unique_iff

deleted theorem function.surjective.exists

deleted theorem function.surjective.exists₂

deleted theorem function.surjective.exists₃

deleted theorem function.surjective.forall

deleted theorem function.surjective.forall₂

deleted theorem function.surjective.forall₃