[Merged by Bors] - refactor(RingTheory/HopfAlgebra): ofConvInverse constructor

[hawkrobe]

The antipode of a Hopf algebra is generally the two-sided inverse of the identity in the convolution algebra End(A). When A is commutative, algebra homs are closed under convolution and this lifts to AlgHom equality. See this comment on #31898.

---

Sadly the AlgHom-equality formulation is unavailable in the noncommutative case.

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary bd33e0a4c9

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ ofAlgHom
+ ofConvInverse
- HopfAlgebra.ofAlgHom

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit bd33e0a4c9
Reference commit 23bafd5167

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[hawkrobe]

@YaelDillies ready for a review when you have the time.

[YaelDillies]

Thanks!

maintainer delegate

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[faenuccio]

@hawkrobe You've got a missing doc string causing CI to fail. Can you please fix this?

[hawkrobe]

@faenuccio fixed, sorry about that!

[faenuccio]

I find the use of anonymous dot notation a bit hard to parse in this definition where it appears as third/fourth variable. Can you replace .all with Commute.all?

[YaelDillies]

This is your personal preference, Filippo. I don't think it's worth mentioning on other people's PRs.

Anonymous dot notation was created precisely for the purpose of being short. Lean code isn't designed to be readable without the infoview.

[eric-wieser]

@YaelDillies, remember that reviewers are free to express and argue their personal preference when the style guide is ambiguous, and I would encourage you to avoid dismissing such comments on the basis of them being preference. Short discussions of conflicting personal preference should not hold up PRs, but the discussion is still worth briefly having in case it leads to clarification of the style guide.

Having said that, I do think using .all is fine here, especially as this is a proof term and not data where perceived ambiguity could even matter.

[hawkrobe]

I fixed the names (and everything else raised in review)!

-awaiting-author

[hawkrobe]

leanprover/lean4#13636 changed simpa behavior and broke the build. i kept the old behavior with using! but I'm not sure whether that's discouraged?

[grunweg]

I think using using! for now is fine.

[YaelDillies]

Thanks! 🚀

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Lint style
• ci (staging) / Build
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job