Skip to content

[Merged by Bors] - feat: port NumberTheory.Cyclotomic.Basic #13702

[Merged by Bors] - feat: port NumberTheory.Cyclotomic.Basic

[Merged by Bors] - feat: port NumberTheory.Cyclotomic.Basic #13702

Triggered via pull request June 22, 2023 08:45
Status Success
Total duration 1m 9s
Artifacts

detect_sha_changes.yml

on: pull_request
Add annotations
1m 0s
Add annotations
Fit to window
Zoom out
Zoom in

Annotations

1 notice
Synchronization: Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean#L7
See https://leanprover-community.github.io/mathlib-port-status/file/linear_algebra/eigenspace/minpoly?range=8efcf8022aac8e01df8d302dcebdbc25d6a886c8..c3216069e5f9369e6be586ccbfcde2592b3cec92