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
    }
}

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_identity_left​

Inherited from AddMonoid.

add_identity_right​

Inherited from AddMonoid.

commutative​

Inherited from AddCommSemigroup.

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.

neg​

Inherited from AddGroup.

sub​

Inherited from AddGroup.