Commit 2025-11-01 19:17 3a5524d0

View on Github →

refactor: simplify InjOn univ f to Injective f (#31024) This follows the pattern set by basically all other pairs of unrestricted/restricted predicates.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Expect.lean

Modified Mathlib/Algebra/BigOperators/Finprod.lean

Modified Mathlib/Data/Fintype/Defs.lean

Modified Mathlib/Data/Set/Function.lean

deleted theorem Function.Surjective.surjOn

added theorem Set.bijOn_univ

modified theorem Set.bijective_iff_bijOn_univ

added theorem Set.injOn_univ

modified theorem Set.injective_iff_injOn_univ

added theorem Set.surjOn_univ

modified theorem Set.surjective_iff_surjOn_univ

Modified Mathlib/Data/Set/Piecewise.lean

Modified Mathlib/Data/Setoid/Partition.lean

Modified Mathlib/FieldTheory/AxGrothendieck.lean

Modified Mathlib/FieldTheory/PrimitiveElement.lean

Modified Mathlib/Geometry/Manifold/WhitneyEmbedding.lean

Modified Mathlib/LinearAlgebra/PID.lean

Modified Mathlib/Logic/Equiv/PartialEquiv.lean

modified theorem PartialEquiv.injective_of_source_eq_univ

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

Modified Mathlib/Order/SupIndep.lean