mathlib3
dfe9e051 - use alias for fields of is_expansion_on

Commit

3 years ago

use alias for fields of is_expansion_on

References

is_expansion_on_alias

Author

fpvandoorn

fpvandoorn

Parents

Loading