Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-04 03:33 acf831c1

View on Github →

chore(algebra/regular/basic): split file (#17179)

Estimated changes

Created src/algebra/hom/embedding.lean

added def mul_left_embedding

added theorem mul_left_embedding_eq_mul_right_embedding

added def mul_right_embedding

Modified src/algebra/hom/ring.lean

Modified src/algebra/regular/basic.lean

deleted def mul_left_embedding

deleted theorem mul_left_embedding_eq_mul_right_embedding

deleted def mul_right_embedding

Modified src/data/finset/basic.lean

Modified src/data/nat/basic.lean

deleted theorem nat.range_cases_on

deleted theorem nat.range_of_succ

deleted theorem nat.range_rec

deleted theorem nat.subtype.coe_bot

deleted theorem nat.zero_union_range_succ

Modified src/data/nat/cast.lean

Modified src/data/nat/order.lean

added theorem nat.range_cases_on

added theorem nat.range_of_succ

added theorem nat.range_rec

added theorem nat.subtype.coe_bot

added theorem nat.zero_union_range_succ

Modified src/data/nat/psub.lean

Modified src/order/complete_lattice.lean

Modified src/order/conditionally_complete_lattice.lean