fake module doc

Mathlib/Algebra/Order/Incidence.lean

@@ -10,6 +10,10 @@ import Mathlib.Algebra.Module.BigOperators
 import Mathlib.Algebra.Module.Pi
 import Mathlib.Order.Interval.Finset.Defs
 
+/-! -/
+-- fake module docstring just so that I can disable the long line linter without getting linted for
+-- a missing module docstring!
+
 set_option linter.style.longLine false in
 /-!
 # Incidence algebras
@@ -53,7 +57,7 @@ Here are some additions to this file that could be made in the future:
 
 open Finset OrderDual
 
-variable {𝕄 F 𝕜 𝕝 𝕞 α β : Type*}
+variable {F 𝕜 𝕝 𝕞 α β : Type*}
 
 /-- The `𝕜`-incidence algebra over `α`. -/
 structure IncidenceAlgebra (𝕜 α : Type*) [Zero 𝕜] [LE α] where
@@ -299,14 +303,10 @@ variable (𝕜) [Zero 𝕜] [One 𝕜] [Preorder α] [@DecidableRel α (· ⩿ 
 
 /-- The lambda function of the incidence algebra is the function that assigns `1` to every nonempty
 interval of cardinality one or two. -/
+@[simps]
 def lambda : IncidenceAlgebra 𝕜 α :=
   ⟨fun a b ↦ if a ⩿ b then 1 else 0, fun _a _b h ↦ if_neg fun hh ↦ h hh.le⟩
 
-variable {𝕜}
-
--- TODO: Can't this be autogenerated?
-@[simp] lemma lambda_apply (a b : α) : lambda 𝕜 a b = if a ⩿ b then 1 else 0 := rfl
-
 end Lambda
 
 /-! ### The Zeta and Möbius functions -/