Skip to content

Commit

Permalink
style(Algebra/Module/Injective): fix weird bracket position (#8589)
Browse files Browse the repository at this point in the history
The bracket position seems off
  • Loading branch information
jjaassoonn committed Nov 23, 2023
1 parent 40cf206 commit e9bcfc6
Showing 1 changed file with 1 addition and 2 deletions.
3 changes: 1 addition & 2 deletions Mathlib/Algebra/Module/Injective.lean
Expand Up @@ -175,8 +175,7 @@ set_option linter.uppercaseLean3 false in
/-- The maximal element of every nonempty chain of `extension_of i f`. -/
def ExtensionOf.max {c : Set (ExtensionOf i f)} (hchain : IsChain (· ≤ ·) c)
(hnonempty : c.Nonempty) : ExtensionOf i f :=
{
LinearPMap.sSup _
{ LinearPMap.sSup _
(IsChain.directedOn <|
chain_linearPMap_of_chain_extensionOf
hchain) with
Expand Down

0 comments on commit e9bcfc6

Please sign in to comment.