Commit 2023-10-25 17:48 0eda3bbc
View on Github →fix(CategoryTheory/Monoidal/Category): correct mathport-ized lemma names (#7923)
tensor_hom_inv_id
, which matches tensor_inv_hom_id
, was incorrectly renamed during porting to tensorHom_inv_id
.
fix(CategoryTheory/Monoidal/Category): correct mathport-ized lemma names (#7923)
tensor_hom_inv_id
, which matches tensor_inv_hom_id
, was incorrectly renamed during porting to tensorHom_inv_id
.