From 81381ad8339f8f2b075d0846b3d11fd3ecca4e75 Mon Sep 17 00:00:00 2001 From: "Filippo A. E. Nuccio" Date: Fri, 22 Nov 2024 11:21:14 +0000 Subject: [PATCH] doc(Algebra/Central/Defs): correct doc (#19363) Correct two typos and a bad syntax in the doc. --- Mathlib/Algebra/Central/Defs.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/Central/Defs.lean b/Mathlib/Algebra/Central/Defs.lean index c88a10b8b3aba..363464e22abef 100644 --- a/Mathlib/Algebra/Central/Defs.lean +++ b/Mathlib/Algebra/Central/Defs.lean @@ -19,7 +19,7 @@ is a (not necessarily commutative) `K`-algebra. ## Implementation notes We require the `K`-center of `D` to be smaller than or equal to the smallest subalgebra so that when -we prove something is central, there we don't need to prove `⊥ ≤ center K D` even though this +we prove something is central, we don't need to prove `⊥ ≤ center K D` even though this direction is trivial. ### Central Simple Algebras @@ -34,11 +34,11 @@ but an instance of `[Algebra.IsCentralSimple K D]` would not imply `[IsSimpleRin synthesization orders (`K` cannot be inferred). Thus, to obtain a central simple `K`-algebra `D`, one should use `Algebra.IsCentral K D` and `IsSimpleRing D` separately. -Note that the predicate `Albgera.IsCentral K D` and `IsSimpleRing D` makes sense just for `K` a +Note that the predicate `Algebra.IsCentral K D` and `IsSimpleRing D` makes sense just for `K` a `CommRing` but it doesn't give the right definition for central simple algebra; for a commutative ring base, one should use the theory of Azumaya algebras. In fact ideals of `K` immediately give rise to nontrivial quotients of `D` so there are no central simple algebras in this case according -to our definition, if K is not a field. +to our definition, if `K` is not a field. The theory of central simple algebras really is a theory over fields. Thus to declare a central simple algebra, one should use the following: