Scalar3.mmL: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar3.bend as Scalar3 Lines 47-48 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar3.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar3.bend&start_line=47&end_line=48 import Base import bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend as SE def mmL(+one: Nat) -> Nat: Nat.sub(SE.ell(one), 1n) Uses (3): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend&name=ell