[Merged by Bors] - feat: port Algebra.Hom.NonUnitalAlg

[jcommelin]

---

[ocfnash]

There are currently no build errors but six linter errors, all from the simpNF linter. These six come in pairs associated to the definitions of NonUnitalAlgHom.fst, NonUnitalAlgHom.snd, NonUnitalAlgHom.prod.

The errors can be solved by writing three simp lemmas manually instead of using simps (as shown in suggestions). It would be good to know if this is a limitation of simps or a case of pilot error.

In particular it would be good to understand why simps is generating lemmas of the form:

NonUnitalAlgHom.fst_toDistribMulActionHom_toMulActionHom_toFun

[fpvandoorn]

There are currently no build errors but six linter errors, all from the simpNF linter. These six come in pairs associated to the definitions of NonUnitalAlgHom.fst, NonUnitalAlgHom.snd, NonUnitalAlgHom.prod.

The errors can be solved by writing three simp lemmas manually instead of using simps (as shown in suggestions). It would be good to know if this is a limitation of simps or a case of pilot error.

In particular it would be good to understand why simps is generating lemmas of the form:

NonUnitalAlgHom.fst_toDistribMulActionHom_toMulActionHom_toFun

This is just a misconfiguration.
The initialize_simps_projections needs a -toDistribMulActionHom argument. Also, you probably want to define a custom NonUnitalAlgHom.Simps.apply. Mimic the code of MonoidHom or something. Or merge #2045, after which no custom configuration is needed at all.

[ocfnash]

Thanks @fpvandoorn

What do we need to do to get #2045 / #2042 merged? Are they just waiting for final review?

[jcommelin]

Thanks 🎉

bors merge

[eric-wieser]

Suggested change

	theorem mk_coe (f : A →ₙₐ[R] B) (h₁ h₂ h₃ h₄) : (⟨⟨⟨f, h₁⟩, h₂, h₃⟩, h₄⟩ : A →ₙₐ[R] B) = f := by
	theorem mk_coe (f : A →ₙₐ[R] B) (h₁ h₂ h₃ h₄) : (⟨⟨⟨f, h₁⟩, h₂, h₃⟩, h₄⟩ : A →ₙₐ[R] B) = f :=

and similarly elsewhere

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style