On 2017-08-24 09:38, Thiemann, Rene wrote:
If one imports HOL-Algebra.Multiplicative_Group (which we actually
do
via some transitive import), then \mu (LFP), \nu (GFP) and
\phi (Euler’s totient function) become constants.
Unless I hear otherwise I will replace \mu by LFP and \nu by GFP.
On 2017-08-31 13:54, Florian Haftmann wrote:
The theorem in question requires both the notion of subgroup and
complete lattices, hence the import order dictates in which theory the
theorem has to reside (btw. the current import order is similar to
HOL-Main where Complete_Lattices comes after Gro
