Skip to content

Commit

Permalink
fix(RingTheory.Kaehler): fix map docstring (#11459)
Browse files Browse the repository at this point in the history
  • Loading branch information
@kbuzzard @utensil
kbuzzard authored and utensil committed Mar 26, 2024
1 parent 50b60c3 commit ec26de6
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/RingTheory/Kaehler.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
↑ ↑
| |
Expand Down

0 comments on commit ec26de6

Please sign in to comment.