Commit 2021-04-25 03:55 d5330fe8

View on Github →

chore(algebra/category): remove duplicated proofs (#7349) The results added in #7100 already exist. I moved them to the place where Scott added the duplicates. Hopefully that will make them more discoverable.

Estimated changes

Modified src/algebra/category/Module/basic.lean

deleted theorem Module.epi_of_range_eq_top

deleted theorem Module.ker_eq_bot_of_mono

deleted theorem Module.mono_of_ker_eq_bot

deleted theorem Module.range_eq_top_of_epi

Modified src/algebra/category/Module/epi_mono.lean

added theorem Module.epi_iff_range_eq_top

modified theorem Module.epi_iff_surjective

added theorem Module.ker_eq_bot_of_mono

modified theorem Module.mono_iff_injective

added theorem Module.mono_iff_ker_eq_bot

added theorem Module.range_eq_top_of_epi

Modified src/algebra/category/Module/kernels.lean

Modified src/algebra/category/Module/subobject.lean