Skip to content

Commit 5cad90b

Browse files
committed
chore(Algebra): move QuadraticAlgebra to QuadraticAlgebra/Defs (#31490)
Since we already have a `QuadraticAlgebra` folder, this should go in there. It looks strange on the documentation otherwise.
1 parent 109eba6 commit 5cad90b

File tree

3 files changed

+2
-2
lines changed

3 files changed

+2
-2
lines changed

Mathlib.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1084,8 +1084,8 @@ import Mathlib.Algebra.Polynomial.UnitTrinomial
10841084
import Mathlib.Algebra.PresentedMonoid.Basic
10851085
import Mathlib.Algebra.Prime.Defs
10861086
import Mathlib.Algebra.Prime.Lemmas
1087-
import Mathlib.Algebra.QuadraticAlgebra
10881087
import Mathlib.Algebra.QuadraticAlgebra.Basic
1088+
import Mathlib.Algebra.QuadraticAlgebra.Defs
10891089
import Mathlib.Algebra.QuadraticDiscriminant
10901090
import Mathlib.Algebra.Quandle
10911091
import Mathlib.Algebra.Quaternion

Mathlib/Algebra/QuadraticAlgebra/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Antoine Chambert-Loir
55
-/
66

7-
import Mathlib.Algebra.QuadraticAlgebra
7+
import Mathlib.Algebra.QuadraticAlgebra.Defs
88
import Mathlib.Algebra.Star.Unitary
99
import Mathlib.Tactic.FieldSimp
1010

File renamed without changes.

0 commit comments

Comments
 (0)