Commit 2026-06-30 06:44 e695991a

View on Github →

feat(FormalGroup): F(X,0)=X and F(0,X)=X (#38052) In this PR, I prove that given a formal group law F, then F(X,0) = X and F(0,X) = X. And modify the definition of FormalGroup.Point to be a subtype. And prove that this subtype is a AddZeroClass. Eventually we will prove that this is a AddGroup.

Estimated changes

modified def FormalGroup.Point
added theorem FormalGroup.Xzero_eq_X
added theorem FormalGroup.add_apply
added theorem FormalGroup.add_zero
added theorem FormalGroup.assoc'
added theorem FormalGroup.comm'
added theorem FormalGroup.zeroX_eq_X
added theorem FormalGroup.zero_add
added theorem FormalGroup.zero_apply