From ec26de6bf6249812443d6d3c93c2a8acb15a3f82 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Mon, 18 Mar 2024 16:28:50 +0000 Subject: [PATCH] fix(RingTheory.Kaehler): fix map docstring (#11459) --- Mathlib/RingTheory/Kaehler.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Kaehler.lean b/Mathlib/RingTheory/Kaehler.lean index 0137ed9012b9bc..199d747e12c384 100644 --- a/Mathlib/RingTheory/Kaehler.lean +++ b/Mathlib/RingTheory/Kaehler.lean @@ -638,7 +638,7 @@ variable [Algebra A B] [Algebra S B] [IsScalarTower R A B] [IsScalarTower R S B] variable [SMulCommClass S A B] -/-- The map `Ω[A⁄R] →ₗ[A] Ω[B⁄R]` given a square +/-- The map `Ω[A⁄R] →ₗ[A] Ω[B⁄S]` given a square A --→ B ↑ ↑ | |