We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent bdface9 commit 1589a31Copy full SHA for 1589a31
1 file changed
Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean
@@ -74,7 +74,7 @@ lemma mapDomainBialgHom_id : mapDomainBialgHom R (.id M) = .id R R[M] := by ext;
74
@[to_additive (attr := simp)]
75
lemma mapDomainBialgHom_comp (f : N →* O) (g : M →* N) :
76
mapDomainBialgHom R (f.comp g) = (mapDomainBialgHom R f).comp (mapDomainBialgHom R g) := by
77
- ext; simp [Finsupp.mapDomain_comp]
+ ext; simp [Finsupp.mapDomain_fun_comp]
78
79
@[to_additive]
80
lemma mapDomainBialgHom_mapDomainBialgHom (f : N →* O) (g : M →* N) (x : R[M]) :
0 commit comments