mathlib
491c492a - show `star_alg_hom`s and friends are order preserving for `star_ordered_ring`s

Commit

3 years ago

show `star_alg_hom`s and friends are order preserving for `star_ordered_ring`s

Author

j-loreaux

j-loreaux

Parents

Loading