/-! ファミリーと多項式 -/ /- →《《《《《《《《《《《《《《《《《《《《 → -/ namespace My /- 型コンストラクタ Fam -/ def Fam (X : Type) := X → Type abbrev FamOver := Fam variable (I : Type) (i j : I) variable (F G : FamOver I) def Sigm {X: …
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。