[Merged by Bors] - feat: maps between the unitization of a non-unital subalgebra and its Algebra.adjoin
#18000
j-loreauxdetect_sha_changes.yml
on: pull_request
Add annotations
28s
Annotations
1 notice
|
Synchronization:
Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean#L8
See review instructions and diff at
https://leanprover-community.github.io/mathlib-port-status/file/algebraic_topology/dold_kan/compatibility?range=160f568dcf772b2477791c844fc605f2f91f73d1..18ee599842a5d17f189fe572f0ed8cb1d064d772
|