2021-03-04 21:18
src/algebra/linear_ordered_comm_group_with_zero.lean
feat(algebra/ordered_*, */sub{monoid,group,ring,semiring,field,algebra}): pullback of ordered algebraic structures under an injective map (#6489) …
Added function.injective.linear_ordered_comm_monoid_with_zero