Skip to main content

Field

typeclass F: Field extends CommRing, Inverse {
    field_inverse_zero {
        F.0.inverse = F.0
    }
    field_inverse(f: F) {
        f != F.0 implies f * f.inverse = F.1
    }
    zero_and_one_are_distinct {
        F.0 != F.1
    }
}

A field is a commutative ring with multiplicative inverses for all non-zero elements.

GitHub

add​

Inherited from Add.

add_associative​

Inherited from AddSemigroup.

add_commutative​

Inherited from AddCommSemigroup.

add_identity_left​

Inherited from AddMonoid.

add_identity_right​

Inherited from AddMonoid.

commutative​

Inherited from CommSemigroup.

distrib_left​

Inherited from Semiring.

distrib_right​

Inherited from Semiring.

field_inverse​

field_inverse(f: F) {
    f != F.0 implies f * f.inverse = F.1
}

The definition of "multiplicative inverse" in a field.

field_inverse_zero​

field_inverse_zero {
    F.0.inverse = F.0
}

We define the field inverse so that the inverse of zero is zero. It would be nice to instead express that an inverse is "not valid" or yields "no value" but it is not convenient to do so in the current type system.

inverse​

Inherited from Inverse.

inverse_right​

Inherited from AddGroup.

mul​

Inherited from Mul.

mul_associative​

Inherited from Semigroup.

mul_identity_left​

Inherited from Monoid.

mul_identity_right​

Inherited from Monoid.

mul_zero_left​

Inherited from Semiring.

mul_zero_right​

Inherited from Semiring.

neg​

Inherited from Neg.

pow​

Inherited from Monoid.

sub​

Inherited from AddGroup.

zero_and_one_are_distinct​

zero_and_one_are_distinct {
    F.0 != F.1
}

Zero and one are distinct elements.

zpow​

define zpow(self, exp: Int) -> F {
    match exp {
        Int.from_nat(n) {
            self.pow(n)
        }
        Int.neg_suc(k) {
            self.pow(k.suc).inverse
        }
    }
}

Extends Monoid.pow to raise a field element to an integer. Similar to how we define Field.inverse this defines F.0.zpow(x) for negative x to be 0.