KeyPair.mk.{u_1, u_2} {FType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {GType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  FType u_1]
  [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  GType u_2] [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  FType u_1 GType u_2] {G₀G : GType u_2}
  (privF : FType u_1) (pubG : GType u_2)
  (pub_eqpub = DH priv G₀ : pubG =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. DHDH.{u_1, u_2} {F : Type u_1} [Field F] {G : Type u_2} [AddCommGroup G] [Module F G] (a : F) (B : G) : GDiffie-Hellman function: DH(a, B) = a • B.  privF G₀G) :
  KeyPairKeyPair.{u_1, u_2} (F : Type u_1) (G : Type u_2) [Field F] [AddCommGroup G] [Module F G] (G₀ : G) : Type (max u_1 u_2)A key pair: private scalar and public group element satisfying
pub = DH(priv, G₀). The paper defines four key types: identity (IK),
signed prekey (SPK), one-time prekey (OPK), and ephemeral (EK).  FType u_1 GType u_2 G₀G