Commit 2022-08-10 13:06 16cf14f1

View on Github →

feat(number_theory/cyclotomic/rat): add integral_power_basis (#15570) We add integral_power_basis and some variants, defining integral power basis of 𝓞 K. From flt-regular

Estimated changes

Modified src/number_theory/cyclotomic/rat.lean

added theorem is_primitive_root.integral_power_basis'_gen

added theorem is_primitive_root.integral_power_basis_dim

added theorem is_primitive_root.integral_power_basis_gen

added theorem is_primitive_root.power_basis_int'_dim

added theorem is_primitive_root.sub_one_integral_power_basis'_gen

added theorem is_primitive_root.sub_one_integral_power_basis_gen

Modified src/number_theory/number_field.lean

added theorem number_field.is_integral_of_mem_ring_of_integers