Commit 2024-09-25 15:52 5f551d9f

View on Github →

chore(Set/Image): rename 2 lemmas (#17134) Use existsUnique, not exists_unique in 2 lemmas

Estimated changes

Modified Mathlib/Data/Fintype/Basic.lean

Modified Mathlib/Data/Set/Image.lean

deleted theorem Function.Injective.exists_unique_of_mem_range

added theorem Function.Injective.mem_range_iff_existsUnique

deleted theorem Function.Injective.mem_range_iff_exists_unique

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean