[math-fun] That sqrt7 product again