Skip to content

[Merged by Bors] - feat: define ProperConstSMul #21250

[Merged by Bors] - feat: define ProperConstSMul

[Merged by Bors] - feat: define ProperConstSMul #21250

Triggered via pull request August 30, 2023 15:07
Status Success
Total duration 1m 1s
Artifacts

detect_sha_changes.yml

on: pull_request
Add annotations
37s
Add annotations
Fit to window
Zoom out
Zoom in

Annotations

10 notices
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=18ee599842a5d17f189fe572f0ed8cb1d064d772..32a7e535287f9c73f2e4d2aef306a39190f0b504
Synchronization: Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean#L8
See review instructions and diff at https://leanprover-community.github.io/mathlib-port-status/file/algebraic_topology/dold_kan/decomposition?range=9af20344b24ef1801b599d296aaed8b9fffdc360..32a7e535287f9c73f2e4d2aef306a39190f0b504
Synchronization: Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean#L9
See review instructions and diff at https://leanprover-community.github.io/mathlib-port-status/file/algebraic_topology/dold_kan/degeneracies?range=ec1c7d810034d4202b0dd239112d1792be9f6fdc..32a7e535287f9c73f2e4d2aef306a39190f0b504
Synchronization: Mathlib/AlgebraicTopology/DoldKan/EquivalenceAdditive.lean#L8
See review instructions and diff at https://leanprover-community.github.io/mathlib-port-status/file/algebraic_topology/dold_kan/equivalence_additive?range=19d6240dcc5e5c8bd6e1e3c588b92e837af76f9e..32a7e535287f9c73f2e4d2aef306a39190f0b504
Synchronization: Mathlib/AlgebraicTopology/DoldKan/EquivalencePseudoabelian.lean#L10
See review instructions and diff at https://leanprover-community.github.io/mathlib-port-status/file/algebraic_topology/dold_kan/equivalence_pseudoabelian?range=63721b2c3eba6c325ecf8ae8cca27155a4f6306f..32a7e535287f9c73f2e4d2aef306a39190f0b504
Synchronization: Mathlib/AlgebraicTopology/DoldKan/Faces.lean#L8
See review instructions and diff at https://leanprover-community.github.io/mathlib-port-status/file/algebraic_topology/dold_kan/faces?range=70fd9563a21e7b963887c9360bd29b2393e6225a..32a7e535287f9c73f2e4d2aef306a39190f0b504
Synchronization: Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean#L8
See review instructions and diff at https://leanprover-community.github.io/mathlib-port-status/file/algebraic_topology/dold_kan/functor_gamma?range=5b8284148e8149728f4b90624888d98c36284454..32a7e535287f9c73f2e4d2aef306a39190f0b504
Synchronization: Mathlib/AlgebraicTopology/DoldKan/FunctorN.lean#L8
See review instructions and diff at https://leanprover-community.github.io/mathlib-port-status/file/algebraic_topology/dold_kan/functor_n?range=1995c7bbdbb0adb1b6d5acdc654f6cf46ed96cfa..32a7e535287f9c73f2e4d2aef306a39190f0b504
Synchronization: Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean#L9
See review instructions and diff at https://leanprover-community.github.io/mathlib-port-status/file/algebraic_topology/dold_kan/gamma_comp_n?range=5f68029a863bdf76029fa0f7a519e6163c14152e..32a7e535287f9c73f2e4d2aef306a39190f0b504
Synchronization: Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean#L9
See review instructions and diff at https://leanprover-community.github.io/mathlib-port-status/file/algebraic_topology/dold_kan/n_comp_gamma?range=19d6240dcc5e5c8bd6e1e3c588b92e837af76f9e..32a7e535287f9c73f2e4d2aef306a39190f0b504