Invariant/variant boucle

Bonjour,

Je suis en licence et débutante en programmation sur python.
J'ai un exercice à rendre mais je ne comprends pas bien certains points.

Après avoir écrit la définition de factorielle, on me demande de trouver un invariant et un variant de boucle.

Ma définition est :

def factorielle(n):
’’’ int -> int
Hypothèse : n > 0
Retourne le produit factoriel n!’’’
# k : int
k = 1 # on demarre au rang 1
# f : int
f = 1 # factorielle au rang 1
while k <= n:
f = f * k
k = k + 1
return f

Comme invariant j'ai pensé : f = 1*(f-1)*f

Voila, j'aimerais que l'on puisse me dire si je suis sur la bonne voie pour l'invariant...et comment trouver le variant.

Je vous remercie.