docstring

dagurtomas · Oct 1, 2024 · b6c7975 · b6c7975
1 parent f45532a
commit b6c7975
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/LeanCondensed/Projects/LightSolid.lean b/LeanCondensed/Projects/LightSolid.lean
@@ -130,6 +130,8 @@ abbrev induced_from_one_minus_shift (A : LightCondMod R) :
 
 variable {R : Type} [CommRing R]
 
+/-- A light condensed `R`-module `A` is *solid* if the shift map `ℕ∪∞ → ℕ∪∞` induces an isomorphism
+on internal homs into `A` -/
 class IsSolid (A : LightCondMod R) : Prop where
   one_minus_shift_induces_iso : IsIso ((pre (one_minus_shift R)).app A)