Skip to content

gmap_view_auth: add fraction

Ralf Jung requested to merge ralf/gmap-view-auth-frac into master

I followed the style of auth to only have one definition with the fraction, but have a bunch of lemmas for the special case q = 1. I am not sure if these lemmas carry their weight, but well, now that we already have them I figured we could keep them.

Fixes #356 (closed)

Merge request reports