Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ring_hom.star_def

Modification history

2022-12-23 08:51
src/algebra/star/basic.lean
feat(number_theory/number_field/embeddings) : add infinite_places (#17844) …
Modified ring_hom.star_defView on Github →
2022-12-14 21:31
src/algebra/star/basic.lean
feat(algebra/star/basic): add ring_hom.has_involutive_star (#17904) …
Added ring_hom.star_defView on Github →