Skip to main content

Field

typeclass F: Field extends CommRing {
    inverse: F -> F
    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 AddSemigroup.

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​

inverse: F -> F

The multiplicative inverse function.

inverse_right​

Inherited from AddGroup.

mul​

Inherited from Semigroup.

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 AddGroup.

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.