Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-06 05:41 2e140f1e

View on Github →

refactor(algebra/inj_surj): more lemmas, move to files, rename (#3290)

use names function.?jective.monoid etc;
move definitions to different files;
add versions for semimodules and various *_with_zero;
add funciton.surjective.forall etc.

Estimated changes

Created src/algebra/group/inj_surj.lean

Modified src/algebra/group_with_zero.lean

Deleted src/algebra/inj_surj.lean

deleted def comm_group_of_injective

deleted def comm_group_of_surjective

deleted def comm_monoid_of_injective

deleted def comm_monoid_of_surjective

deleted def comm_ring_of_injective

deleted def comm_ring_of_surjective

deleted def comm_semigroup_of_injective

deleted def comm_semigroup_of_surjective

deleted def comm_semiring_of_injective

deleted def comm_semiring_of_surjective

deleted def group_of_injective

deleted def group_of_surjective

deleted def monoid_of_injective

deleted def monoid_of_surjective

deleted def ring_of_injective

deleted def ring_of_surjective

deleted def semigroup_of_injective

deleted def semigroup_of_surjective

deleted def semiring_of_injective

deleted def semiring_of_surjective

Modified src/algebra/module.lean

Modified src/algebra/ring.lean

modified theorem ring_hom.cancel_left

modified theorem ring_hom.cancel_right

Modified src/group_theory/group_action.lean

deleted theorem mul_action.bijective

Modified src/group_theory/submonoid/basic.lean

added theorem submonoid.coe_injective

Modified src/group_theory/submonoid/operations.lean

Modified src/logic/function/basic.lean

added theorem function.injective.eq_iff'

added theorem function.injective.ne_iff'

added theorem function.surjective.exists

added theorem function.surjective.exists₂

added theorem function.surjective.exists₃

added theorem function.surjective.forall

added theorem function.surjective.forall₂

added theorem function.surjective.forall₃