Re: [isabelle] Period of tangent



> in fact the period of tangent is pi, which is also provable as:
> 
> lemma tan_periodic [simp] : "!! x . tan (x) = tan(x + pi)"
> by (simp add: tan_def)

We'll add this and more general versions, although in the other
direction to avoid looping.

Thanks
Tobias





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.